author | nipkow |

Wed Mar 14 17:38:49 2001 +0100 (2001-03-14) | |

changeset 11205 | 67cec35dbc58 |

parent 11204 | bb01189f0565 |

child 11206 | 5bea3a8abdc3 |

*** empty log message ***

doc-src/TutorialI/basics.tex | file | annotate | diff | revisions | |

doc-src/TutorialI/todo.tobias | file | annotate | diff | revisions | |

doc-src/manual.bib | file | annotate | diff | revisions |

1.1 --- a/doc-src/TutorialI/basics.tex Wed Mar 14 08:50:55 2001 +0100 1.2 +++ b/doc-src/TutorialI/basics.tex Wed Mar 14 17:38:49 2001 +0100 1.3 @@ -17,12 +17,15 @@ 1.4 misled: HOL can express most mathematical concepts, and functional programming 1.5 is just one particularly simple and ubiquitous instance. 1.6 1.7 -Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. 1.8 -This has influenced some of HOL's concrete syntax but is otherwise 1.9 -irrelevant for us because this tutorial is based on 1.10 -Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle 1.11 -with structured proofs.\footnote{Thus the full name of the system should be 1.12 - Isabelle/Isar/HOL, but that is a bit of a mouthful.} 1.13 +Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has 1.14 +influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant 1.15 +for us because this tutorial is based on 1.16 +Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle with 1.17 +structured proofs. Thus the full name of the system should be 1.18 +Isabelle/Isar/HOL, but that is a bit of a mouthful. There are other 1.19 +implementations of HOL, in particular the one by Mike Gordon \emph{et al.}, 1.20 +which is usually referred to as ``the HOL system'' \cite{mgordon-hol}. For us, 1.21 +HOL refers to the logical system, and sometimes its incarnation Isabelle/HOL. 1.22 1.23 A tutorial is by definition incomplete. Currently the tutorial only 1.24 introduces the rudiments of Isar's proof language. To fully exploit the power

2.1 --- a/doc-src/TutorialI/todo.tobias Wed Mar 14 08:50:55 2001 +0100 2.2 +++ b/doc-src/TutorialI/todo.tobias Wed Mar 14 17:38:49 2001 +0100 2.3 @@ -57,12 +57,6 @@ 2.4 2.5 Advanced recdef: explain recdef_tc? 2.6 2.7 -I guess we should say "HOL" everywhere, with a remark early on about the 2.8 -differences between our HOL and the other one. 2.9 - 2.10 -Syntax translations! Harpoons already used! 2.11 -say something about "abbreviations" when defs are introduced. 2.12 - 2.13 warning: simp of asms from l to r; may require reordering (rotate_tac) 2.14 2.15 Adjust FP textbook refs: new Bird, Hudak

3.1 --- a/doc-src/manual.bib Wed Mar 14 08:50:55 2001 +0100 3.2 +++ b/doc-src/manual.bib Wed Mar 14 17:38:49 2001 +0100 3.3 @@ -91,8 +91,13 @@ 3.4 @InProceedings{Aspinall:TACAS:2000, 3.5 author = {David Aspinall}, 3.6 title = {{P}roof {G}eneral: A Generic Tool for Proof Development}, 3.7 - booktitle = {ETAPS / TACAS}, 3.8 - year = 2000 3.9 + booktitle = {Tools and Algorithms for the Construction and Analysis of 3.10 + Systems (TACAS)}, 3.11 + year = 2000, 3.12 + publisher = Springer, 3.13 + series = LNCS, 3.14 + volume = 1785, 3.15 + pages = "38--42" 3.16 } 3.17 3.18 @Misc{isamode, 3.19 @@ -335,7 +340,7 @@ 3.20 note = {Translated by Yves LaFont and Paul Taylor}} 3.21 3.22 @Book{mgordon-hol, 3.23 - author = {M. J. C. Gordon and T. F. Melham}, 3.24 + editor = {M. J. C. Gordon and T. F. Melham}, 3.25 title = {Introduction to {HOL}: A Theorem Proving Environment for 3.26 Higher Order Logic}, 3.27 publisher = CUP,