equal
deleted
inserted
replaced
32 its incarnation Isabelle/HOL\@. |
32 its incarnation Isabelle/HOL\@. |
33 |
33 |
34 A tutorial is by definition incomplete. Currently the tutorial only |
34 A tutorial is by definition incomplete. Currently the tutorial only |
35 introduces the rudiments of Isar's proof language. To fully exploit the power |
35 introduces the rudiments of Isar's proof language. To fully exploit the power |
36 of Isar, in particular the ability to write readable and structured proofs, |
36 of Isar, in particular the ability to write readable and structured proofs, |
37 you need to consult the Isabelle/Isar Reference |
37 you should start with Nipkow's overview~\cite{Nipkow-TYPES02} and consult |
38 Manual~\cite{isabelle-isar-ref} and Wenzel's PhD thesis~\cite{Wenzel-PhD} |
38 the Isabelle/Isar Reference Manual~\cite{isabelle-isar-ref} and Wenzel's |
39 which discusses many proof patterns. If you want to use Isabelle's ML level |
39 PhD thesis~\cite{Wenzel-PhD} (which discusses many proof patterns) |
|
40 for further details. If you want to use Isabelle's ML level |
40 directly (for example for writing your own proof procedures) see the Isabelle |
41 directly (for example for writing your own proof procedures) see the Isabelle |
41 Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the |
42 Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the |
42 Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive |
43 Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive |
43 index. |
44 index. |
44 |
45 |