A Tactic Language for Declarative Proofs

@inproceedings{pub4917,
    author = {

Autexier, Serge
 and 

Dietrich, Dominik
},
    editor = {

Kaufmann, Matt
 and 

Paulson, Lawrence C.
},
    title = {A Tactic Language for Declarative Proofs},
    booktitle = {Proceedings International Conference on Interactive Theorem Proving. International Conference on Interactive Theorem Proving (ITP-2010), July 11-14, Edinburgh, United Kingdom},
    series = {Lecture Notes in Computer Sciences (LNCS)},
    year = {2010},
    month = {7},
    volume = {6172},
    pages = {99--114},
    publisher = {Springer}
}