2 @string{CUCL="Comp. Lab., Univ. Camb."} |
2 @string{CUCL="Comp. Lab., Univ. Camb."} |
3 @string{CUP="Cambridge University Press"} |
3 @string{CUP="Cambridge University Press"} |
4 @string{Springer="Springer-Verlag"} |
4 @string{Springer="Springer-Verlag"} |
5 @string{TUM="TU Munich"} |
5 @string{TUM="TU Munich"} |
6 |
6 |
|
7 |
|
8 @InProceedings{Wenzel:1999:TPHOL, |
|
9 author = {Markus Wenzel}, |
|
10 title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents}, |
|
11 crossref = {tphols99}} |
7 |
12 |
8 @Book{davey-priestley, |
13 @Book{davey-priestley, |
9 author = {B. A. Davey and H. A. Priestley}, |
14 author = {B. A. Davey and H. A. Priestley}, |
10 title = {Introduction to Lattices and Order}, |
15 title = {Introduction to Lattices and Order}, |
11 publisher = CUP, |
16 publisher = CUP, |
22 title = {Introduction to {Isabelle}}, |
27 title = {Introduction to {Isabelle}}, |
23 institution = CUCL} |
28 institution = CUCL} |
24 |
29 |
25 @manual{isabelle-isar-ref, |
30 @manual{isabelle-isar-ref, |
26 author = {Markus Wenzel}, |
31 author = {Markus Wenzel}, |
27 title = {The {Isabelle Isar} Reference Manual}, |
32 title = {The {Isabelle/Isar} Reference Manual}, |
28 institution = TUM} |
33 institution = TUM} |
29 |
34 |
30 @InProceedings{Wenzel:1999:TPHOL, |
35 @manual{isabelle-ref, |
31 author = {Markus Wenzel}, |
36 author = {Lawrence C. Paulson}, |
32 title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents}, |
37 title = {The {Isabelle} Reference Manual}, |
33 crossref = {tphols99}} |
38 institution = CUCL} |
|
39 |
|
40 @TechReport{paulson-mutilated-board, |
|
41 author = {Lawrence C. Paulson}, |
|
42 title = {A Simple Formalization and Proof for the Mutilated Chess Board}, |
|
43 institution = CUCL, |
|
44 year = 1996, |
|
45 number = 394, |
|
46 note = {\url{http://www.ftp.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.pdf}} |
|
47 } |
34 |
48 |
35 @Proceedings{tphols99, |
49 @Proceedings{tphols99, |
36 title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, |
50 title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, |
37 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, |
51 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, |
38 editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and |
52 editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and |