| 47269 |      1 | @string{CUP="Cambridge University Press"}
 | 
|  |      2 | @string{LNCS="Lect.\ Notes in Comp.\ Sci."}
 | 
| 65348 |      3 | @string{Springer="Springer"}
 | 
|  |      4 | 
 | 
|  |      5 | @InProceedings{BauerW-TPHOLs01,author={Gertrud Bauer and Markus Wenzel},
 | 
|  |      6 | title={Calculational Reasoning Revisited --- An {Isabelle/Isar} Experience},
 | 
|  |      7 | booktitle={Theorem Proving in Higher Order Logics, TPHOLs 2001},
 | 
|  |      8 | editor={R. Boulton and P. Jackson},
 | 
|  |      9 | year=2001,publisher=Springer,series=LNCS,volume=2152,pages="75--90"}
 | 
| 47269 |     10 | 
 | 
|  |     11 | @book{HuthRyan,author="Michael Huth and Mark Ryan",
 | 
|  |     12 | title={Logic in Computer Science},publisher=CUP,year=2004}
 | 
|  |     13 | 
 | 
|  |     14 | @manual{Krauss,author={Alexander Krauss},
 | 
|  |     15 | title={Defining Recursive Functions in Isabelle/HOL},
 | 
| 68649 |     16 | note={\url{https://isabelle.in.tum.de/doc/functions.pdf}}}
 | 
| 47269 |     17 | 
 | 
| 51784 |     18 | @manual{Nipkow-Main,author={Tobias Nipkow},title={What's in Main},
 | 
| 68649 |     19 | note={\url{https://isabelle.in.tum.de/doc/main.pdf}}}
 | 
| 51784 |     20 | 
 | 
| 47269 |     21 | @book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
 | 
|  |     22 | title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
 | 
|  |     23 | publisher=Springer,series=LNCS,volume=2283,year=2002}
 | 
|  |     24 | 
 | 
| 52782 |     25 | @book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
 | 
| 59317 |     26 | title="Concrete Semantics with Isabelle/HOL",publisher="Springer",year=2014,
 | 
|  |     27 | note={298 pp. \url{http://concrete-semantics.org}}}
 | 
| 52782 |     28 | 
 | 
| 47269 |     29 | @manual{IsarRef,author={Makarius Wenzel},
 | 
|  |     30 | title={The Isabelle/Isar Reference Manual},
 | 
| 68649 |     31 | note={\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}}
 |