|
1 |
|
2 @string{CUCL="Comp. Lab., Univ. Camb."} |
|
3 @string{CUP="Cambridge University Press"} |
|
4 @string{Springer="Springer-Verlag"} |
|
5 @string{TUM="TU Munich"} |
|
6 |
|
7 |
|
8 @Book{davey-priestley, |
|
9 author = {B. A. Davey and H. A. Priestley}, |
|
10 title = {Introduction to Lattices and Order}, |
|
11 publisher = CUP, |
|
12 year = 1990} |
|
13 |
|
14 @manual{isabelle-HOL, |
|
15 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, |
|
16 title = {{Isabelle}'s Logics: {HOL}}, |
|
17 institution = {Institut f\"ur Informatik, Technische Universi\"at |
|
18 M\"unchen and Computer Laboratory, University of Cambridge}} |
|
19 |
|
20 @manual{isabelle-intro, |
|
21 author = {Lawrence C. Paulson}, |
|
22 title = {Introduction to {Isabelle}}, |
|
23 institution = CUCL} |
|
24 |
|
25 @manual{isabelle-isar-ref, |
|
26 author = {Markus Wenzel}, |
|
27 title = {The {Isabelle Isar} Reference Manual}, |
|
28 institution = TUM} |
|
29 |
|
30 @InProceedings{Wenzel:1999:TPHOL, |
|
31 author = {Markus Wenzel}, |
|
32 title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents}, |
|
33 crossref = {tphols99}} |
|
34 |
|
35 @Proceedings{tphols99, |
|
36 title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, |
|
37 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, |
|
38 editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and |
|
39 Paulin, C. and Thery, L.}, |
|
40 series = {LNCS 1690}, |
|
41 year = 1999} |