author | nipkow |

Mon Mar 19 12:38:36 2001 +0100 (2001-03-19) | |

changeset 11213 | aeb5c72dd72a |

parent 11212 | d06fb91f22da |

child 11214 | 3b3cc0cf533f |

*** empty log message ***

1.1 --- a/doc-src/TutorialI/Types/Overloading0.thy Mon Mar 19 10:37:47 2001 +0100 1.2 +++ b/doc-src/TutorialI/Types/Overloading0.thy Mon Mar 19 12:38:36 2001 +0100 1.3 @@ -33,7 +33,7 @@ 1.4 warnings to that effect. 1.5 1.6 However, there is nothing to prevent the user from forming terms such as 1.7 -@{text"inverse []"} and proving theorems as @{text"inverse [] 1.8 +@{text"inverse []"} and proving theorems such as @{text"inverse [] 1.9 = inverse []"}, although we never defined inverse on lists. We hasten to say 1.10 that there is nothing wrong with such terms and theorems. But it would be 1.11 nice if we could prevent their formation, simply because it is very likely

2.1 --- a/doc-src/TutorialI/Types/document/Overloading0.tex Mon Mar 19 10:37:47 2001 +0100 2.2 +++ b/doc-src/TutorialI/Types/document/Overloading0.tex Mon Mar 19 12:38:36 2001 +0100 2.3 @@ -37,7 +37,7 @@ 2.4 warnings to that effect. 2.5 2.6 However, there is nothing to prevent the user from forming terms such as 2.7 -\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}}, although we never defined inverse on lists. We hasten to say 2.8 +\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}}, although we never defined inverse on lists. We hasten to say 2.9 that there is nothing wrong with such terms and theorems. But it would be 2.10 nice if we could prevent their formation, simply because it is very likely 2.11 that the user did not mean to write what he did. Thus she had better not waste

3.1 --- a/doc-src/TutorialI/Types/types.tex Mon Mar 19 10:37:47 2001 +0100 3.2 +++ b/doc-src/TutorialI/Types/types.tex Mon Mar 19 12:38:36 2001 +0100 3.3 @@ -43,7 +43,7 @@ 3.4 Isabelle offers the related concept of an \textbf{axiomatic type class}. 3.5 Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\ 3.6 an axiomatic specification of a class of types. Thus we can talk about a type 3.7 -$t$ being in a class $C$, which is written $\tau :: C$. This is the case if 3.8 +$\tau$ being in a class $C$, which is written $\tau :: C$. This is the case if 3.9 $\tau$ satisfies the axioms of $C$. Furthermore, type classes can be 3.10 organized in a hierarchy. Thus there is the notion of a class $D$ being a 3.11 \textbf{subclass} of a class $C$, written $D < C$. This is the case if all

4.1 --- a/doc-src/TutorialI/basics.tex Mon Mar 19 10:37:47 2001 +0100 4.2 +++ b/doc-src/TutorialI/basics.tex Mon Mar 19 12:38:36 2001 +0100 4.3 @@ -20,16 +20,19 @@ 4.4 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has 4.5 influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant 4.6 for us because this tutorial is based on 4.7 -Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle with 4.8 -structured proofs. Thus the full name of the system should be 4.9 -Isabelle/Isar/HOL, but that is a bit of a mouthful. There are other 4.10 -implementations of HOL, in particular the one by Mike Gordon \emph{et al.}, 4.11 -which is usually referred to as ``the HOL system'' \cite{mgordon-hol}. For us, 4.12 -HOL refers to the logical system, and sometimes its incarnation Isabelle/HOL. 4.13 +Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides 4.14 +the implementation language almost completely. Thus the full name of the 4.15 +system should be Isabelle/Isar/HOL, but that is a bit of a mouthful. 4.16 + 4.17 +There are other implementations of HOL, in particular the one by Mike Gordon 4.18 +\emph{et al.}, which is usually referred to as ``the HOL system'' 4.19 +\cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes 4.20 +its incarnation Isabelle/HOL. 4.21 4.22 A tutorial is by definition incomplete. Currently the tutorial only 4.23 introduces the rudiments of Isar's proof language. To fully exploit the power 4.24 -of Isar you need to consult the Isabelle/Isar Reference 4.25 +of Isar, in particular the ability to write readable and structured proofs, 4.26 +you need to consult the Isabelle/Isar Reference 4.27 Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level 4.28 directly (for example for writing your own proof procedures) see the Isabelle 4.29 Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the

5.1 --- a/doc-src/TutorialI/fp.tex Mon Mar 19 10:37:47 2001 +0100 5.2 +++ b/doc-src/TutorialI/fp.tex Mon Mar 19 12:38:36 2001 +0100 5.3 @@ -284,7 +284,7 @@ 5.4 (except real axioms) is reduced to a definition. For example, given some 5.5 \isacommand{primrec} function definition, this is turned into a proper 5.6 (nonrecursive!) definition, and the user-supplied recursion equations are 5.7 -derived as theorems from the definition. This tricky process is completely 5.8 +derived as theorems from that definition. This tricky process is completely 5.9 hidden from the user and it is not necessary to understand the details. The 5.10 result of the definitional approach is that \isacommand{primrec} is as safe 5.11 as pure \isacommand{defs} are, but more convenient. And this is not just the

6.1 --- a/doc-src/TutorialI/tutorial.tex Mon Mar 19 10:37:47 2001 +0100 6.2 +++ b/doc-src/TutorialI/tutorial.tex Mon Mar 19 12:38:36 2001 +0100 6.3 @@ -77,8 +77,8 @@ 6.4 \subsubsection*{Acknowledgements} 6.5 This tutorial owes a lot to the constant discussions with and the valuable 6.6 feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf M{\"u}ller, 6.7 -Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch 6.8 -and Markus Wenzel. Stephan Merz was also kind enough to 6.9 +Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch, 6.10 +Martin Strecker and Markus Wenzel. Stephan Merz was also kind enough to 6.11 read and comment on a draft version. 6.12 \clearfirst 6.13