equal
deleted
inserted
replaced
124 title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental |
124 title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental |
125 Comparison}, |
125 Comparison}, |
126 crossref = {huet-plotkin91}, |
126 crossref = {huet-plotkin91}, |
127 pages = {89-119}} |
127 pages = {89-119}} |
128 |
128 |
|
129 @Unpublished{HOL-Library, |
|
130 author = {Gertrud Bauer and Tobias Nipkow and Oheimb, David von and |
|
131 Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and |
|
132 Markus Wenzel}, |
|
133 title = {The Supplemental {Isabelle/HOL} Library}, |
|
134 note = {Part of the Isabelle2001 distribution, |
|
135 \url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}}, |
|
136 year = 2001 |
|
137 } |
|
138 |
129 @InProceedings{Bauer-Wenzel:2000:HB, |
139 @InProceedings{Bauer-Wenzel:2000:HB, |
130 author = {Gertrud Bauer and Markus Wenzel}, |
140 author = {Gertrud Bauer and Markus Wenzel}, |
131 title = {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in |
141 title = {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in |
132 {I}sabelle/{I}sar}, |
142 {I}sabelle/{I}sar}, |
133 booktitle = {Types for Proofs and Programs: TYPES'99}, |
143 booktitle = {Types for Proofs and Programs: TYPES'99}, |