A Tactic Language for Declarative Proofs<pre>@inproceedings{AD-10-a,
  author        = {Serge Autexier and Dominik Dietrich},
  editor        = {Matt Kaufmann and Lawrence C. Paulson},
  booktitle     = {Proceedings International Conference on Interactive Theorem Proving
},
  title         = {A Tactic Language for Declarative Proofs},
  volume        = {6172},
  series        = {LNCS},
  publisher     = {Springer},
  address       = {Edinburgh, Scotland},
  pages         = {99-114},
  month         = {july},
  year          = {2010},
}
</pre>