--- a/latex/cpdt.bib	Thu Apr 12 14:30:53 2012 -0400
+++ b/latex/cpdt.bib	Thu Apr 12 15:54:37 2012 -0400
@@ -360,3 +360,18 @@
 booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {2010},
 }
+
+@inproceedings{Isar,
+ author = {Wenzel, Markus},
+ title = {Isar - A Generic Interpretative Approach to Readable Formal Proof Documents},
+ booktitle = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics},
+ series = {TPHOLs '99},
+ year = {1999},
+ isbn = {3-540-66463-7},
+ pages = {167--184},
+ numpages = {18},
+ url = {http://dl.acm.org/citation.cfm?id=646526.694887},
+ acmid = {694887},
+ publisher = {Springer-Verlag},
+ address = {London, UK, UK},
+}