36 year = 2001, |
36 year = 2001, |
37 note = {Part of the Isabelle distribution, |
37 note = {Part of the Isabelle distribution, |
38 \url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}} |
38 \url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}} |
39 } |
39 } |
40 |
40 |
|
41 @Article{Paulson:1989, |
|
42 author = {L. C. Paulson}, |
|
43 title = {The foundation of a generic Theorem Prover}, |
|
44 journal = {Journal of Automated Reasoning}, |
|
45 year = 1989, |
|
46 volume = 5, |
|
47 number = 3, |
|
48 pages = {363--397} |
|
49 } |
|
50 |
41 @InProceedings{Wenzel:1999, |
51 @InProceedings{Wenzel:1999, |
42 author = {Markus Wenzel}, |
52 author = {Markus Wenzel}, |
43 title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents}, |
53 title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents}, |
44 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, |
54 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, |
45 editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and |
55 editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and |