initial setup for chapter on document preparation;
authorwenzelm
Mon Oct 01 14:44:00 2001 +0200 (2001-10-01)
changeset 116470538cb0f7999
parent 11646 6a7d80a139c6
child 11648 d78a82d112e4
initial setup for chapter on document preparation;
doc-src/TutorialI/Documents/Documents.thy
doc-src/TutorialI/Documents/ROOT.ML
doc-src/TutorialI/Documents/document/root.tex
doc-src/TutorialI/Documents/documents.tex
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Makefile
doc-src/TutorialI/tutorial.ind
doc-src/TutorialI/tutorial.tex
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/Documents/Documents.thy	Mon Oct 01 14:44:00 2001 +0200
     1.3 @@ -0,0 +1,7 @@
     1.4 +(*<*)
     1.5 +theory Documents = Main:
     1.6 +(*>*)
     1.7 +
     1.8 +(*<*)
     1.9 +end
    1.10 +(*>*)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/TutorialI/Documents/ROOT.ML	Mon Oct 01 14:44:00 2001 +0200
     2.3 @@ -0,0 +1,2 @@
     2.4 +
     2.5 +use_thy "Documents";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/TutorialI/Documents/document/root.tex	Mon Oct 01 14:44:00 2001 +0200
     3.3 @@ -0,0 +1,4 @@
     3.4 +\documentclass{article}
     3.5 +\begin{document}
     3.6 +xxx
     3.7 +\end{document}
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/TutorialI/Documents/documents.tex	Mon Oct 01 14:44:00 2001 +0200
     4.3 @@ -0,0 +1,10 @@
     4.4 +
     4.5 +\chapter{Document preparation}
     4.6 +
     4.7 +\input{Documents/document/Documents.tex}
     4.8 +
     4.9 +
    4.10 +%%% Local Variables: 
    4.11 +%%% mode: latex
    4.12 +%%% TeX-master: t
    4.13 +%%% End: 
     5.1 --- a/doc-src/TutorialI/IsaMakefile	Mon Oct 01 14:42:47 2001 +0200
     5.2 +++ b/doc-src/TutorialI/IsaMakefile	Mon Oct 01 14:44:00 2001 +0200
     5.3 @@ -4,7 +4,9 @@
     5.4  
     5.5  ## targets
     5.6  
     5.7 -default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Real-Types HOL-Misc HOL-Protocol styles
     5.8 +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef \
     5.9 +  HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Real-Types HOL-Misc \
    5.10 +  HOL-Protocol HOL-Documents styles
    5.11  images:
    5.12  test:
    5.13  all: default
    5.14 @@ -185,7 +187,15 @@
    5.15  	$(USEDIR) Protocol
    5.16  	@rm -f tutorial.dvi
    5.17  
    5.18 +## HOL-Documents
    5.19 +
    5.20 +HOL-Documents: HOL $(LOG)/HOL-Documents.gz
    5.21 +
    5.22 +$(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML
    5.23 +	$(USEDIR) Documents
    5.24 +	@rm -f tutorial.dvi
    5.25 +
    5.26  ## clean
    5.27  
    5.28  clean:
    5.29 -	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz Rules/document/*.tex Sets/document/*.tex
    5.30 +	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz $(LOG)/HOL-Documents.gz Rules/document/*.tex Sets/document/*.tex
     6.1 --- a/doc-src/TutorialI/Makefile	Mon Oct 01 14:42:47 2001 +0200
     6.2 +++ b/doc-src/TutorialI/Makefile	Mon Oct 01 14:44:00 2001 +0200
     6.3 @@ -22,6 +22,7 @@
     6.4  	Protocol/protocol.tex \
     6.5  	Rules/rules.tex Sets/sets.tex \
     6.6  	Types/numerics.tex Types/records.tex Types/types.tex \
     6.7 +	Documents/documents.tex \
     6.8  	../iman.sty ../ttbox.sty ../extra.sty \
     6.9  	isabelle.sty isabellesym.sty ../pdfsetup.sty
    6.10  
     7.1 --- a/doc-src/TutorialI/tutorial.ind	Mon Oct 01 14:42:47 2001 +0200
     7.2 +++ b/doc-src/TutorialI/tutorial.ind	Mon Oct 01 14:44:00 2001 +0200
     7.3 @@ -1,630 +1,630 @@
     7.4  \begin{theindex}
     7.5  
     7.6 -  \item \ttall, \bold{187}
     7.7 -  \item \texttt{?}, \bold{187}
     7.8 -  \item \isasymuniqex, \bold{187}
     7.9 -  \item \ttuniquex, \bold{187}
    7.10 -  \item {\texttt {\&}}, \bold{187}
    7.11 -  \item \verb$~$, \bold{187}
    7.12 -  \item \verb$~=$, \bold{187}
    7.13 -  \item \ttor, \bold{187}
    7.14 -  \item \texttt{[]}, \bold{7}
    7.15 -  \item \texttt{\#}, \bold{7}
    7.16 -  \item \texttt{\at}, \bold{8}, 187
    7.17 -  \item \isasymnotin, \bold{187}
    7.18 -  \item \verb$~:$, \bold{187}
    7.19 -  \item \isasymInter, \bold{187}
    7.20 -  \item \isasymUnion, \bold{187}
    7.21 -  \item \isasyminverse, \bold{187}
    7.22 -  \item \verb$^-1$, \bold{187}
    7.23 -  \item \isactrlsup{\isacharasterisk}, \bold{187}
    7.24 -  \item \verb$^$\texttt{*}, \bold{187}
    7.25 -  \item \isasymAnd, \bold{10}, \bold{187}
    7.26 -  \item \ttAnd, \bold{187}
    7.27 -  \item \isasymrightleftharpoons, 24
    7.28 -  \item \isasymrightharpoonup, 24
    7.29 -  \item \isasymleftharpoondown, 24
    7.30 -  \item \emph {$\Rightarrow $}, \bold{3}
    7.31 -  \item \ttlbr, \bold{187}
    7.32 -  \item \ttrbr, \bold{187}
    7.33 -  \item \texttt {\%}, \bold{187}
    7.34 -  \item \texttt {;}, \bold{5}
    7.35 -  \item \isa {()} (constant), 22
    7.36 -  \item \isa {+} (tactical), 83
    7.37 +  \item \ttall, \bold{195}
    7.38 +  \item \texttt{?}, \bold{195}
    7.39 +  \item \isasymuniqex, \bold{195}
    7.40 +  \item \ttuniquex, \bold{195}
    7.41 +  \item {\texttt {\&}}, \bold{195}
    7.42 +  \item \verb$~$, \bold{195}
    7.43 +  \item \verb$~=$, \bold{195}
    7.44 +  \item \ttor, \bold{195}
    7.45 +  \item \texttt{[]}, \bold{9}
    7.46 +  \item \texttt{\#}, \bold{9}
    7.47 +  \item \texttt{\at}, \bold{10}, 195
    7.48 +  \item \isasymnotin, \bold{195}
    7.49 +  \item \verb$~:$, \bold{195}
    7.50 +  \item \isasymInter, \bold{195}
    7.51 +  \item \isasymUnion, \bold{195}
    7.52 +  \item \isasyminverse, \bold{195}
    7.53 +  \item \verb$^-1$, \bold{195}
    7.54 +  \item \isactrlsup{\isacharasterisk}, \bold{195}
    7.55 +  \item \verb$^$\texttt{*}, \bold{195}
    7.56 +  \item \isasymAnd, \bold{12}, \bold{195}
    7.57 +  \item \ttAnd, \bold{195}
    7.58 +  \item \isasymrightleftharpoons, 26
    7.59 +  \item \isasymrightharpoonup, 26
    7.60 +  \item \isasymleftharpoondown, 26
    7.61 +  \item \emph {$\Rightarrow $}, \bold{5}
    7.62 +  \item \ttlbr, \bold{195}
    7.63 +  \item \ttrbr, \bold{195}
    7.64 +  \item \texttt {\%}, \bold{195}
    7.65 +  \item \texttt {;}, \bold{7}
    7.66 +  \item \isa {()} (constant), 24
    7.67 +  \item \isa {+} (tactical), 89
    7.68    \item \isa {<*lex*>}, \see{lexicographic product}{1}
    7.69 -  \item \isa {?} (tactical), 83
    7.70 -  \item \texttt{|} (tactical), 83
    7.71 +  \item \isa {?} (tactical), 89
    7.72 +  \item \texttt{|} (tactical), 89
    7.73  
    7.74    \indexspace
    7.75  
    7.76 -  \item \isa {0} (constant), 20, 21, 133
    7.77 -  \item \isa {1} (symbol), 133
    7.78 -  \item \isa {2} (symbol), 133
    7.79 +  \item \isa {0} (constant), 22, 23, 141
    7.80 +  \item \isa {1} (symbol), 141
    7.81 +  \item \isa {2} (symbol), 141
    7.82  
    7.83    \indexspace
    7.84  
    7.85 -  \item abandoning a proof, \bold{11}
    7.86 -  \item abandoning a theory, \bold{14}
    7.87 -  \item \isa {abs} (constant), 135
    7.88 -  \item \texttt {abs}, \bold{187}
    7.89 -  \item absolute value, 135
    7.90 -  \item \isa {add} (modifier), 27
    7.91 -  \item \isa {add_ac} (theorems), 134
    7.92 -  \item \isa {add_assoc} (theorem), \bold{134}
    7.93 -  \item \isa {add_commute} (theorem), \bold{134}
    7.94 -  \item \isa {add_mult_distrib} (theorem), \bold{133}
    7.95 -  \item \texttt {ALL}, \bold{187}
    7.96 -  \item \isa {All} (constant), 93
    7.97 -  \item \isa {allE} (theorem), \bold{65}
    7.98 -  \item \isa {allI} (theorem), \bold{64}
    7.99 -  \item append function, 8--12
   7.100 -  \item \isacommand {apply} (command), 13
   7.101 -  \item \isa {arg_cong} (theorem), \bold{80}
   7.102 -  \item \isa {arith} (method), 21, 131
   7.103 +  \item abandoning a proof, \bold{13}
   7.104 +  \item abandoning a theory, \bold{16}
   7.105 +  \item \isa {abs} (constant), 143
   7.106 +  \item \texttt {abs}, \bold{195}
   7.107 +  \item absolute value, 143
   7.108 +  \item \isa {add} (modifier), 29
   7.109 +  \item \isa {add_ac} (theorems), 142
   7.110 +  \item \isa {add_assoc} (theorem), \bold{142}
   7.111 +  \item \isa {add_commute} (theorem), \bold{142}
   7.112 +  \item \isa {add_mult_distrib} (theorem), \bold{141}
   7.113 +  \item \texttt {ALL}, \bold{195}
   7.114 +  \item \isa {All} (constant), 99
   7.115 +  \item \isa {allE} (theorem), \bold{71}
   7.116 +  \item \isa {allI} (theorem), \bold{70}
   7.117 +  \item append function, 10--14
   7.118 +  \item \isacommand {apply} (command), 15
   7.119 +  \item \isa {arg_cong} (theorem), \bold{86}
   7.120 +  \item \isa {arith} (method), 23, 139
   7.121    \item arithmetic operations
   7.122 -    \subitem for \protect\isa{nat}, 21
   7.123 -  \item \textsc {ascii} symbols, \bold{187}
   7.124 -  \item associative-commutative function, 156
   7.125 -  \item \isa {assumption} (method), 53
   7.126 +    \subitem for \protect\isa{nat}, 23
   7.127 +  \item \textsc {ascii} symbols, \bold{195}
   7.128 +  \item associative-commutative function, 164
   7.129 +  \item \isa {assumption} (method), 59
   7.130    \item assumptions
   7.131 -    \subitem of subgoal, 10
   7.132 -    \subitem renaming, 66--67
   7.133 -    \subitem reusing, 67
   7.134 -  \item \isa {auto} (method), 35, 76
   7.135 -  \item \isa {axclass}, 144--150
   7.136 -  \item axiom of choice, 70
   7.137 -  \item axiomatic type classes, 144--150
   7.138 +    \subitem of subgoal, 12
   7.139 +    \subitem renaming, 72--73
   7.140 +    \subitem reusing, 73
   7.141 +  \item \isa {auto} (method), 37, 82
   7.142 +  \item \isa {axclass}, 152--158
   7.143 +  \item axiom of choice, 76
   7.144 +  \item axiomatic type classes, 152--158
   7.145  
   7.146    \indexspace
   7.147  
   7.148 -  \item \isacommand {back} (command), 62
   7.149 -  \item \isa {Ball} (constant), 93
   7.150 -  \item \isa {ballI} (theorem), \bold{92}
   7.151 -  \item \isa {best} (method), 76
   7.152 -  \item \isa {Bex} (constant), 93
   7.153 -  \item \isa {bexE} (theorem), \bold{92}
   7.154 -  \item \isa {bexI} (theorem), \bold{92}
   7.155 -  \item \isa {bij_def} (theorem), \bold{94}
   7.156 -  \item bijections, 94
   7.157 -  \item binary trees, 16
   7.158 -  \item binomial coefficients, 93
   7.159 -  \item bisimulations, 100
   7.160 -  \item \isa {blast} (method), 73--74, 76
   7.161 -  \item \isa {bool} (type), 2, 3
   7.162 -  \item boolean expressions example, 18--20
   7.163 -  \item \isa {bspec} (theorem), \bold{92}
   7.164 -  \item \isacommand{by} (command), 57
   7.165 +  \item \isacommand {back} (command), 68
   7.166 +  \item \isa {Ball} (constant), 99
   7.167 +  \item \isa {ballI} (theorem), \bold{98}
   7.168 +  \item \isa {best} (method), 82
   7.169 +  \item \isa {Bex} (constant), 99
   7.170 +  \item \isa {bexE} (theorem), \bold{98}
   7.171 +  \item \isa {bexI} (theorem), \bold{98}
   7.172 +  \item \isa {bij_def} (theorem), \bold{100}
   7.173 +  \item bijections, 100
   7.174 +  \item binary trees, 18
   7.175 +  \item binomial coefficients, 99
   7.176 +  \item bisimulations, 106
   7.177 +  \item \isa {blast} (method), 79--80, 82
   7.178 +  \item \isa {bool} (type), 4, 5
   7.179 +  \item boolean expressions example, 20--22
   7.180 +  \item \isa {bspec} (theorem), \bold{98}
   7.181 +  \item \isacommand{by} (command), 63
   7.182  
   7.183    \indexspace
   7.184  
   7.185 -  \item \isa {card} (constant), 93
   7.186 -  \item \isa {card_Pow} (theorem), \bold{93}
   7.187 -  \item \isa {card_Un_Int} (theorem), \bold{93}
   7.188 -  \item cardinality, 93
   7.189 -  \item \isa {case} (symbol), 30, 31
   7.190 -  \item \isa {case} expressions, 3, 4, 16
   7.191 -  \item case distinctions, 17
   7.192 -  \item case splits, \bold{29}
   7.193 -  \item \isa {case_tac} (method), 17, 85, 139
   7.194 -  \item \isa {clarify} (method), 75, 76
   7.195 -  \item \isa {clarsimp} (method), 75, 76
   7.196 -  \item \isa {classical} (theorem), \bold{57}
   7.197 -  \item coinduction, \bold{100}
   7.198 -  \item \isa {Collect} (constant), 93
   7.199 -  \item \isa {comp_def} (theorem), \bold{96}
   7.200 -  \item compiling expressions example, 34--36
   7.201 -  \item \isa {Compl_iff} (theorem), \bold{90}
   7.202 +  \item \isa {card} (constant), 99
   7.203 +  \item \isa {card_Pow} (theorem), \bold{99}
   7.204 +  \item \isa {card_Un_Int} (theorem), \bold{99}
   7.205 +  \item cardinality, 99
   7.206 +  \item \isa {case} (symbol), 32, 33
   7.207 +  \item \isa {case} expressions, 5, 6, 18
   7.208 +  \item case distinctions, 19
   7.209 +  \item case splits, \bold{31}
   7.210 +  \item \isa {case_tac} (method), 19, 91, 147
   7.211 +  \item \isa {clarify} (method), 81, 82
   7.212 +  \item \isa {clarsimp} (method), 81, 82
   7.213 +  \item \isa {classical} (theorem), \bold{63}
   7.214 +  \item coinduction, \bold{106}
   7.215 +  \item \isa {Collect} (constant), 99
   7.216 +  \item \isa {comp_def} (theorem), \bold{102}
   7.217 +  \item compiling expressions example, 36--38
   7.218 +  \item \isa {Compl_iff} (theorem), \bold{96}
   7.219    \item complement
   7.220 -    \subitem of a set, 89
   7.221 +    \subitem of a set, 95
   7.222    \item composition
   7.223 -    \subitem of functions, \bold{94}
   7.224 -    \subitem of relations, \bold{96}
   7.225 +    \subitem of functions, \bold{100}
   7.226 +    \subitem of relations, \bold{102}
   7.227    \item conclusion
   7.228 -    \subitem of subgoal, 10
   7.229 +    \subitem of subgoal, 12
   7.230    \item conditional expressions, \see{\isa{if} expressions}{1}
   7.231 -  \item conditional simplification rules, 29
   7.232 -  \item \isa {cong} (attribute), 156
   7.233 -  \item congruence rules, \bold{155}
   7.234 -  \item \isa {conjE} (theorem), \bold{55}
   7.235 -  \item \isa {conjI} (theorem), \bold{52}
   7.236 -  \item \isa {Cons} (constant), 7
   7.237 -  \item \isacommand {constdefs} (command), 23
   7.238 -  \item \isacommand {consts} (command), 8
   7.239 -  \item contrapositives, 57
   7.240 +  \item conditional simplification rules, 31
   7.241 +  \item \isa {cong} (attribute), 164
   7.242 +  \item congruence rules, \bold{163}
   7.243 +  \item \isa {conjE} (theorem), \bold{61}
   7.244 +  \item \isa {conjI} (theorem), \bold{58}
   7.245 +  \item \isa {Cons} (constant), 9
   7.246 +  \item \isacommand {constdefs} (command), 25
   7.247 +  \item \isacommand {consts} (command), 10
   7.248 +  \item contrapositives, 63
   7.249    \item converse
   7.250 -    \subitem of a relation, \bold{96}
   7.251 -  \item \isa {converse_iff} (theorem), \bold{96}
   7.252 -  \item CTL, 105--110, 171--173
   7.253 +    \subitem of a relation, \bold{102}
   7.254 +  \item \isa {converse_iff} (theorem), \bold{102}
   7.255 +  \item CTL, 111--116, 179--181
   7.256  
   7.257    \indexspace
   7.258  
   7.259 -  \item \isacommand {datatype} (command), 7, 36--41
   7.260 -  \item datatypes, 15--20
   7.261 -    \subitem and nested recursion, 38, 42
   7.262 -    \subitem mutually recursive, 36
   7.263 -    \subitem nested, 160
   7.264 -  \item \isacommand {defer} (command), 14, 84
   7.265 -  \item Definitional Approach, 24
   7.266 -  \item definitions, \bold{23}
   7.267 -    \subitem unfolding, \bold{28}
   7.268 -  \item \isacommand {defs} (command), 23
   7.269 -  \item \isa {del} (modifier), 27
   7.270 -  \item description operators, 69--71
   7.271 +  \item \isacommand {datatype} (command), 9, 38--43
   7.272 +  \item datatypes, 17--22
   7.273 +    \subitem and nested recursion, 40, 44
   7.274 +    \subitem mutually recursive, 38
   7.275 +    \subitem nested, 168
   7.276 +  \item \isacommand {defer} (command), 16, 90
   7.277 +  \item Definitional Approach, 26
   7.278 +  \item definitions, \bold{25}
   7.279 +    \subitem unfolding, \bold{30}
   7.280 +  \item \isacommand {defs} (command), 25
   7.281 +  \item \isa {del} (modifier), 29
   7.282 +  \item description operators, 75--77
   7.283    \item descriptions
   7.284 -    \subitem definite, 69
   7.285 -    \subitem indefinite, 70
   7.286 -  \item \isa {dest} (attribute), 86
   7.287 -  \item destruction rules, 55
   7.288 -  \item \isa {diff_mult_distrib} (theorem), \bold{133}
   7.289 +    \subitem definite, 75
   7.290 +    \subitem indefinite, 76
   7.291 +  \item \isa {dest} (attribute), 92
   7.292 +  \item destruction rules, 61
   7.293 +  \item \isa {diff_mult_distrib} (theorem), \bold{141}
   7.294    \item difference
   7.295 -    \subitem of sets, \bold{90}
   7.296 -  \item \isa {disjCI} (theorem), \bold{58}
   7.297 -  \item \isa {disjE} (theorem), \bold{54}
   7.298 -  \item \isa {div} (symbol), 21
   7.299 -  \item divides relation, 68, 79, 85--88, 134
   7.300 +    \subitem of sets, \bold{96}
   7.301 +  \item \isa {disjCI} (theorem), \bold{64}
   7.302 +  \item \isa {disjE} (theorem), \bold{60}
   7.303 +  \item \isa {div} (symbol), 23
   7.304 +  \item divides relation, 74, 85, 91--94, 142
   7.305    \item division
   7.306 -    \subitem by negative numbers, 135
   7.307 -    \subitem by zero, 134
   7.308 -    \subitem for type \protect\isa{nat}, 133
   7.309 +    \subitem by negative numbers, 143
   7.310 +    \subitem by zero, 142
   7.311 +    \subitem for type \protect\isa{nat}, 141
   7.312    \item domain
   7.313 -    \subitem of a relation, 96
   7.314 -  \item \isa {Domain_iff} (theorem), \bold{96}
   7.315 -  \item \isacommand {done} (command), 11
   7.316 -  \item \isa {drule_tac} (method), 60, 80
   7.317 -  \item \isa {dvd_add} (theorem), \bold{134}
   7.318 -  \item \isa {dvd_anti_sym} (theorem), \bold{134}
   7.319 -  \item \isa {dvd_def} (theorem), \bold{134}
   7.320 +    \subitem of a relation, 102
   7.321 +  \item \isa {Domain_iff} (theorem), \bold{102}
   7.322 +  \item \isacommand {done} (command), 13
   7.323 +  \item \isa {drule_tac} (method), 66, 86
   7.324 +  \item \isa {dvd_add} (theorem), \bold{142}
   7.325 +  \item \isa {dvd_anti_sym} (theorem), \bold{142}
   7.326 +  \item \isa {dvd_def} (theorem), \bold{142}
   7.327  
   7.328    \indexspace
   7.329  
   7.330 -  \item \isa {elim!} (attribute), 115
   7.331 -  \item elimination rules, 53--54
   7.332 -  \item \isacommand {end} (command), 12
   7.333 -  \item \isa {Eps} (constant), 93
   7.334 -  \item equality, 3
   7.335 -    \subitem of functions, \bold{93}
   7.336 -    \subitem of records, 143
   7.337 -    \subitem of sets, \bold{90}
   7.338 -  \item \isa {equalityE} (theorem), \bold{90}
   7.339 -  \item \isa {equalityI} (theorem), \bold{90}
   7.340 -  \item \isa {erule} (method), 54
   7.341 -  \item \isa {erule_tac} (method), 60
   7.342 -  \item Euclid's algorithm, 85--88
   7.343 +  \item \isa {elim!} (attribute), 121
   7.344 +  \item elimination rules, 59--60
   7.345 +  \item \isacommand {end} (command), 14
   7.346 +  \item \isa {Eps} (constant), 99
   7.347 +  \item equality, 5
   7.348 +    \subitem of functions, \bold{99}
   7.349 +    \subitem of records, 151
   7.350 +    \subitem of sets, \bold{96}
   7.351 +  \item \isa {equalityE} (theorem), \bold{96}
   7.352 +  \item \isa {equalityI} (theorem), \bold{96}
   7.353 +  \item \isa {erule} (method), 60
   7.354 +  \item \isa {erule_tac} (method), 66
   7.355 +  \item Euclid's algorithm, 91--94
   7.356    \item even numbers
   7.357 -    \subitem defining inductively, 111--115
   7.358 -  \item \texttt {EX}, \bold{187}
   7.359 -  \item \isa {Ex} (constant), 93
   7.360 -  \item \isa {exE} (theorem), \bold{66}
   7.361 -  \item \isa {exI} (theorem), \bold{66}
   7.362 -  \item \isa {ext} (theorem), \bold{93}
   7.363 +    \subitem defining inductively, 117--121
   7.364 +  \item \texttt {EX}, \bold{195}
   7.365 +  \item \isa {Ex} (constant), 99
   7.366 +  \item \isa {exE} (theorem), \bold{72}
   7.367 +  \item \isa {exI} (theorem), \bold{72}
   7.368 +  \item \isa {ext} (theorem), \bold{99}
   7.369    \item extensionality
   7.370 -    \subitem for functions, \bold{93, 94}
   7.371 -    \subitem for records, 143
   7.372 -    \subitem for sets, \bold{90}
   7.373 -  \item \ttEXU, \bold{187}
   7.374 +    \subitem for functions, \bold{99, 100}
   7.375 +    \subitem for records, 151
   7.376 +    \subitem for sets, \bold{96}
   7.377 +  \item \ttEXU, \bold{195}
   7.378  
   7.379    \indexspace
   7.380  
   7.381 -  \item \isa {False} (constant), 3
   7.382 -  \item \isa {fast} (method), 76, 108
   7.383 -  \item Fibonacci function, 44
   7.384 -  \item \isa {finite} (symbol), 93
   7.385 -  \item \isa {Finites} (constant), 93
   7.386 -  \item fixed points, 100
   7.387 -  \item flags, 3, 4, 31
   7.388 -    \subitem setting and resetting, 3
   7.389 -  \item \isa {force} (method), 75, 76
   7.390 -  \item formulae, 3
   7.391 -  \item forward proof, 76--82
   7.392 -  \item \isa {frule} (method), 67
   7.393 -  \item \isa {frule_tac} (method), 60
   7.394 -  \item \isa {fst} (constant), 22
   7.395 -  \item function types, 3
   7.396 -  \item functions, 93--95
   7.397 -    \subitem partial, 162
   7.398 -    \subitem total, 9, 44--50
   7.399 -    \subitem underdefined, 163
   7.400 +  \item \isa {False} (constant), 5
   7.401 +  \item \isa {fast} (method), 82, 114
   7.402 +  \item Fibonacci function, 46
   7.403 +  \item \isa {finite} (symbol), 99
   7.404 +  \item \isa {Finites} (constant), 99
   7.405 +  \item fixed points, 106
   7.406 +  \item flags, 5, 6, 33
   7.407 +    \subitem setting and resetting, 5
   7.408 +  \item \isa {force} (method), 81, 82
   7.409 +  \item formulae, 5
   7.410 +  \item forward proof, 82--88
   7.411 +  \item \isa {frule} (method), 73
   7.412 +  \item \isa {frule_tac} (method), 66
   7.413 +  \item \isa {fst} (constant), 24
   7.414 +  \item function types, 5
   7.415 +  \item functions, 99--101
   7.416 +    \subitem partial, 170
   7.417 +    \subitem total, 11, 46--52
   7.418 +    \subitem underdefined, 171
   7.419  
   7.420    \indexspace
   7.421  
   7.422 -  \item \isa {gcd} (constant), 77--78, 85--88
   7.423 -  \item generalizing for induction, 113
   7.424 -  \item generalizing induction formulae, 32
   7.425 -  \item Girard, Jean-Yves, \fnote{55}
   7.426 -  \item Gordon, Mike, 1
   7.427 +  \item \isa {gcd} (constant), 83--84, 91--94
   7.428 +  \item generalizing for induction, 119
   7.429 +  \item generalizing induction formulae, 34
   7.430 +  \item Girard, Jean-Yves, \fnote{61}
   7.431 +  \item Gordon, Mike, 3
   7.432    \item grammars
   7.433 -    \subitem defining inductively, 124--129
   7.434 -  \item ground terms example, 119--124
   7.435 +    \subitem defining inductively, 130--135
   7.436 +  \item ground terms example, 125--130
   7.437  
   7.438    \indexspace
   7.439  
   7.440 -  \item \isa {hd} (constant), 15, 35
   7.441 -  \item Hilbert's $\varepsilon$-operator, 70
   7.442 -  \item HOLCF, 41
   7.443 -  \item Hopcroft, J. E., 129
   7.444 -  \item \isa {hypreal} (type), 137
   7.445 +  \item \isa {hd} (constant), 17, 37
   7.446 +  \item Hilbert's $\varepsilon$-operator, 76
   7.447 +  \item HOLCF, 43
   7.448 +  \item Hopcroft, J. E., 135
   7.449 +  \item \isa {hypreal} (type), 145
   7.450  
   7.451    \indexspace
   7.452  
   7.453 -  \item \isa {Id_def} (theorem), \bold{96}
   7.454 -  \item \isa {id_def} (theorem), \bold{94}
   7.455 -  \item identifiers, \bold{4}
   7.456 -    \subitem qualified, \bold{2}
   7.457 -  \item identity function, \bold{94}
   7.458 -  \item identity relation, \bold{96}
   7.459 -  \item \isa {if} expressions, 3, 4
   7.460 -    \subitem simplification of, 31
   7.461 -    \subitem splitting of, 29, 47
   7.462 -  \item if-and-only-if, 3
   7.463 -  \item \isa {iff} (attribute), 74, 86, 114
   7.464 -  \item \isa {iffD1} (theorem), \bold{78}
   7.465 -  \item \isa {iffD2} (theorem), \bold{78}
   7.466 +  \item \isa {Id_def} (theorem), \bold{102}
   7.467 +  \item \isa {id_def} (theorem), \bold{100}
   7.468 +  \item identifiers, \bold{6}
   7.469 +    \subitem qualified, \bold{4}
   7.470 +  \item identity function, \bold{100}
   7.471 +  \item identity relation, \bold{102}
   7.472 +  \item \isa {if} expressions, 5, 6
   7.473 +    \subitem simplification of, 33
   7.474 +    \subitem splitting of, 31, 49
   7.475 +  \item if-and-only-if, 5
   7.476 +  \item \isa {iff} (attribute), 80, 92, 120
   7.477 +  \item \isa {iffD1} (theorem), \bold{84}
   7.478 +  \item \isa {iffD2} (theorem), \bold{84}
   7.479    \item image
   7.480 -    \subitem under a function, \bold{95}
   7.481 -    \subitem under a relation, \bold{96}
   7.482 -  \item \isa {image_def} (theorem), \bold{95}
   7.483 -  \item \isa {Image_iff} (theorem), \bold{96}
   7.484 -  \item \isa {impI} (theorem), \bold{56}
   7.485 -  \item implication, 56--57
   7.486 -  \item \isa {ind_cases} (method), 115
   7.487 -  \item \isa {induct_tac} (method), 10, 17, 50, 170
   7.488 -  \item induction, 166--173
   7.489 -    \subitem complete, 168
   7.490 -    \subitem deriving new schemas, 170
   7.491 -    \subitem on a term, 167
   7.492 -    \subitem recursion, 49--50
   7.493 -    \subitem structural, 17
   7.494 -    \subitem well-founded, 99
   7.495 -  \item induction heuristics, 31--33
   7.496 -  \item \isacommand {inductive} (command), 111
   7.497 +    \subitem under a function, \bold{101}
   7.498 +    \subitem under a relation, \bold{102}
   7.499 +  \item \isa {image_def} (theorem), \bold{101}
   7.500 +  \item \isa {Image_iff} (theorem), \bold{102}
   7.501 +  \item \isa {impI} (theorem), \bold{62}
   7.502 +  \item implication, 62--63
   7.503 +  \item \isa {ind_cases} (method), 121
   7.504 +  \item \isa {induct_tac} (method), 12, 19, 52, 178
   7.505 +  \item induction, 174--181
   7.506 +    \subitem complete, 176
   7.507 +    \subitem deriving new schemas, 178
   7.508 +    \subitem on a term, 175
   7.509 +    \subitem recursion, 51--52
   7.510 +    \subitem structural, 19
   7.511 +    \subitem well-founded, 105
   7.512 +  \item induction heuristics, 33--35
   7.513 +  \item \isacommand {inductive} (command), 117
   7.514    \item inductive definition
   7.515 -    \subitem simultaneous, 125
   7.516 -  \item inductive definitions, 111--129
   7.517 -  \item \isacommand {inductive\_cases} (command), 115, 123
   7.518 -  \item infinitely branching trees, 40
   7.519 -  \item \isacommand{infixr} (annotation), 8
   7.520 -  \item \isa {inj_on_def} (theorem), \bold{94}
   7.521 -  \item injections, 94
   7.522 -  \item \isa {insert} (constant), 91
   7.523 -  \item \isa {insert} (method), 81--82
   7.524 -  \item instance, \bold{145}
   7.525 -  \item \texttt {INT}, \bold{187}
   7.526 -  \item \texttt {Int}, \bold{187}
   7.527 -  \item \isa {int} (type), 135
   7.528 -  \item \isa {INT_iff} (theorem), \bold{92}
   7.529 -  \item \isa {IntD1} (theorem), \bold{89}
   7.530 -  \item \isa {IntD2} (theorem), \bold{89}
   7.531 -  \item integers, 135
   7.532 -  \item \isa {INTER} (constant), 93
   7.533 -  \item \texttt {Inter}, \bold{187}
   7.534 -  \item \isa {Inter_iff} (theorem), \bold{92}
   7.535 -  \item intersection, 89
   7.536 -    \subitem indexed, 92
   7.537 -  \item \isa {IntI} (theorem), \bold{89}
   7.538 -  \item \isa {intro} (method), 58
   7.539 -  \item \isa {intro!} (attribute), 112
   7.540 -  \item \isa {intro_classes} (method), 145
   7.541 -  \item introduction rules, 52--53
   7.542 -  \item \isa {inv} (constant), 70
   7.543 -  \item \isa {inv_image_def} (theorem), \bold{99}
   7.544 +    \subitem simultaneous, 131
   7.545 +  \item inductive definitions, 117--135
   7.546 +  \item \isacommand {inductive\_cases} (command), 121, 129
   7.547 +  \item infinitely branching trees, 42
   7.548 +  \item \isacommand{infixr} (annotation), 10
   7.549 +  \item \isa {inj_on_def} (theorem), \bold{100}
   7.550 +  \item injections, 100
   7.551 +  \item \isa {insert} (constant), 97
   7.552 +  \item \isa {insert} (method), 87--88
   7.553 +  \item instance, \bold{153}
   7.554 +  \item \texttt {INT}, \bold{195}
   7.555 +  \item \texttt {Int}, \bold{195}
   7.556 +  \item \isa {int} (type), 143
   7.557 +  \item \isa {INT_iff} (theorem), \bold{98}
   7.558 +  \item \isa {IntD1} (theorem), \bold{95}
   7.559 +  \item \isa {IntD2} (theorem), \bold{95}
   7.560 +  \item integers, 143
   7.561 +  \item \isa {INTER} (constant), 99
   7.562 +  \item \texttt {Inter}, \bold{195}
   7.563 +  \item \isa {Inter_iff} (theorem), \bold{98}
   7.564 +  \item intersection, 95
   7.565 +    \subitem indexed, 98
   7.566 +  \item \isa {IntI} (theorem), \bold{95}
   7.567 +  \item \isa {intro} (method), 64
   7.568 +  \item \isa {intro!} (attribute), 118
   7.569 +  \item \isa {intro_classes} (method), 153
   7.570 +  \item introduction rules, 58--59
   7.571 +  \item \isa {inv} (constant), 76
   7.572 +  \item \isa {inv_image_def} (theorem), \bold{105}
   7.573    \item inverse
   7.574 -    \subitem of a function, \bold{94}
   7.575 -    \subitem of a relation, \bold{96}
   7.576 +    \subitem of a function, \bold{100}
   7.577 +    \subitem of a relation, \bold{102}
   7.578    \item inverse image
   7.579 -    \subitem of a function, 95
   7.580 -    \subitem of a relation, 98
   7.581 -  \item \isa {itrev} (constant), 32
   7.582 +    \subitem of a function, 101
   7.583 +    \subitem of a relation, 104
   7.584 +  \item \isa {itrev} (constant), 34
   7.585  
   7.586    \indexspace
   7.587  
   7.588 -  \item \isacommand {kill} (command), 14
   7.589 +  \item \isacommand {kill} (command), 16
   7.590  
   7.591    \indexspace
   7.592  
   7.593 -  \item $\lambda$ expressions, 3
   7.594 -  \item LCF, 41
   7.595 -  \item \isa {LEAST} (symbol), 21, 69
   7.596 -  \item least number operator, \see{\protect\isa{LEAST}}{69}
   7.597 -  \item \isacommand {lemma} (command), 11
   7.598 -  \item \isacommand {lemmas} (command), 77, 86
   7.599 -  \item \isa {length} (symbol), 16
   7.600 -  \item \isa {length_induct}, \bold{170}
   7.601 -  \item \isa {less_than} (constant), 98
   7.602 -  \item \isa {less_than_iff} (theorem), \bold{98}
   7.603 -  \item \isa {let} expressions, 3, 4, 29
   7.604 -  \item \isa {Let_def} (theorem), 29
   7.605 -  \item \isa {lex_prod_def} (theorem), \bold{99}
   7.606 -  \item lexicographic product, \bold{99}, 158
   7.607 +  \item $\lambda$ expressions, 5
   7.608 +  \item LCF, 43
   7.609 +  \item \isa {LEAST} (symbol), 23, 75
   7.610 +  \item least number operator, \see{\protect\isa{LEAST}}{75}
   7.611 +  \item \isacommand {lemma} (command), 13
   7.612 +  \item \isacommand {lemmas} (command), 83, 92
   7.613 +  \item \isa {length} (symbol), 18
   7.614 +  \item \isa {length_induct}, \bold{178}
   7.615 +  \item \isa {less_than} (constant), 104
   7.616 +  \item \isa {less_than_iff} (theorem), \bold{104}
   7.617 +  \item \isa {let} expressions, 5, 6, 31
   7.618 +  \item \isa {Let_def} (theorem), 31
   7.619 +  \item \isa {lex_prod_def} (theorem), \bold{105}
   7.620 +  \item lexicographic product, \bold{105}, 166
   7.621    \item {\texttt{lfp}}
   7.622 -    \subitem applications of, \see{CTL}{100}
   7.623 -  \item linear arithmetic, 20--22, 131
   7.624 -  \item \isa {List} (theory), 15
   7.625 -  \item \isa {list} (type), 2, 7, 15
   7.626 -  \item \isa {list.split} (theorem), 30
   7.627 -  \item \isa {lists_mono} (theorem), \bold{121}
   7.628 -  \item Lowe, Gavin, 176--177
   7.629 +    \subitem applications of, \see{CTL}{106}
   7.630 +  \item linear arithmetic, 22--24, 139
   7.631 +  \item \isa {List} (theory), 17
   7.632 +  \item \isa {list} (type), 4, 9, 17
   7.633 +  \item \isa {list.split} (theorem), 32
   7.634 +  \item \isa {lists_mono} (theorem), \bold{127}
   7.635 +  \item Lowe, Gavin, 184--185
   7.636  
   7.637    \indexspace
   7.638  
   7.639 -  \item \isa {Main} (theory), 2
   7.640 -  \item major premise, \bold{59}
   7.641 -  \item \isa {max} (constant), 21, 22
   7.642 -  \item measure functions, 45, 98
   7.643 -  \item \isa {measure_def} (theorem), \bold{99}
   7.644 -  \item meta-logic, \bold{64}
   7.645 -  \item methods, \bold{14}
   7.646 -  \item \isa {min} (constant), 21, 22
   7.647 -  \item \isa {mod} (symbol), 21
   7.648 -  \item \isa {mod_div_equality} (theorem), \bold{133}
   7.649 -  \item \isa {mod_mult_distrib} (theorem), \bold{133}
   7.650 -  \item model checking example, 100--110
   7.651 -  \item \emph{modus ponens}, 51, 56
   7.652 -  \item \isa {mono_def} (theorem), \bold{100}
   7.653 -  \item monotone functions, \bold{100}, 123
   7.654 -    \subitem and inductive definitions, 121--122
   7.655 -  \item \isa {more} (constant), 140, 141
   7.656 -  \item \isa {mp} (theorem), \bold{56}
   7.657 -  \item \isa {mult_ac} (theorems), 134
   7.658 -  \item multiple inheritance, \bold{149}
   7.659 -  \item multiset ordering, \bold{99}
   7.660 +  \item \isa {Main} (theory), 4
   7.661 +  \item major premise, \bold{65}
   7.662 +  \item \isa {max} (constant), 23, 24
   7.663 +  \item measure functions, 47, 104
   7.664 +  \item \isa {measure_def} (theorem), \bold{105}
   7.665 +  \item meta-logic, \bold{70}
   7.666 +  \item methods, \bold{16}
   7.667 +  \item \isa {min} (constant), 23, 24
   7.668 +  \item \isa {mod} (symbol), 23
   7.669 +  \item \isa {mod_div_equality} (theorem), \bold{141}
   7.670 +  \item \isa {mod_mult_distrib} (theorem), \bold{141}
   7.671 +  \item model checking example, 106--116
   7.672 +  \item \emph{modus ponens}, 57, 62
   7.673 +  \item \isa {mono_def} (theorem), \bold{106}
   7.674 +  \item monotone functions, \bold{106}, 129
   7.675 +    \subitem and inductive definitions, 127--128
   7.676 +  \item \isa {more} (constant), 148, 149
   7.677 +  \item \isa {mp} (theorem), \bold{62}
   7.678 +  \item \isa {mult_ac} (theorems), 142
   7.679 +  \item multiple inheritance, \bold{157}
   7.680 +  \item multiset ordering, \bold{105}
   7.681  
   7.682    \indexspace
   7.683  
   7.684 -  \item \isa {nat} (type), 2, 20, 133--134
   7.685 -  \item \isa {nat_less_induct} (theorem), 168
   7.686 -  \item natural deduction, 51--52
   7.687 -  \item natural numbers, 20, 133--134
   7.688 -  \item Needham-Schroeder protocol, 175--177
   7.689 -  \item negation, 57--59
   7.690 -  \item \isa {Nil} (constant), 7
   7.691 -  \item \isa {no_asm} (modifier), 27
   7.692 -  \item \isa {no_asm_simp} (modifier), 27
   7.693 -  \item \isa {no_asm_use} (modifier), 27
   7.694 -  \item non-standard reals, 137
   7.695 -  \item \isa {None} (constant), \bold{22}
   7.696 -  \item \isa {notE} (theorem), \bold{57}
   7.697 -  \item \isa {notI} (theorem), \bold{57}
   7.698 -  \item numbers, 131--137
   7.699 -  \item numeric literals, 132
   7.700 -    \subitem for type \protect\isa{nat}, 133
   7.701 -    \subitem for type \protect\isa{real}, 136
   7.702 +  \item \isa {nat} (type), 4, 22, 141--142
   7.703 +  \item \isa {nat_less_induct} (theorem), 176
   7.704 +  \item natural deduction, 57--58
   7.705 +  \item natural numbers, 22, 141--142
   7.706 +  \item Needham-Schroeder protocol, 183--185
   7.707 +  \item negation, 63--65
   7.708 +  \item \isa {Nil} (constant), 9
   7.709 +  \item \isa {no_asm} (modifier), 29
   7.710 +  \item \isa {no_asm_simp} (modifier), 29
   7.711 +  \item \isa {no_asm_use} (modifier), 29
   7.712 +  \item non-standard reals, 145
   7.713 +  \item \isa {None} (constant), \bold{24}
   7.714 +  \item \isa {notE} (theorem), \bold{63}
   7.715 +  \item \isa {notI} (theorem), \bold{63}
   7.716 +  \item numbers, 139--145
   7.717 +  \item numeric literals, 140
   7.718 +    \subitem for type \protect\isa{nat}, 141
   7.719 +    \subitem for type \protect\isa{real}, 144
   7.720  
   7.721    \indexspace
   7.722  
   7.723 -  \item \isa {O} (symbol), 96
   7.724 -  \item \texttt {o}, \bold{187}
   7.725 -  \item \isa {o_def} (theorem), \bold{94}
   7.726 -  \item \isa {OF} (attribute), 79--80
   7.727 -  \item \isa {of} (attribute), 77, 80
   7.728 -  \item \isa {only} (modifier), 27
   7.729 -  \item \isacommand {oops} (command), 11
   7.730 -  \item \isa {option} (type), \bold{22}
   7.731 -  \item ordered rewriting, \bold{156}
   7.732 -  \item overloading, 21, 144--146
   7.733 -    \subitem and arithmetic, 132
   7.734 +  \item \isa {O} (symbol), 102
   7.735 +  \item \texttt {o}, \bold{195}
   7.736 +  \item \isa {o_def} (theorem), \bold{100}
   7.737 +  \item \isa {OF} (attribute), 85--86
   7.738 +  \item \isa {of} (attribute), 83, 86
   7.739 +  \item \isa {only} (modifier), 29
   7.740 +  \item \isacommand {oops} (command), 13
   7.741 +  \item \isa {option} (type), \bold{24}
   7.742 +  \item ordered rewriting, \bold{164}
   7.743 +  \item overloading, 23, 152--154
   7.744 +    \subitem and arithmetic, 140
   7.745  
   7.746    \indexspace
   7.747  
   7.748 -  \item pairs and tuples, 22, 137--140
   7.749 -  \item parent theories, \bold{2}
   7.750 +  \item pairs and tuples, 24, 145--148
   7.751 +  \item parent theories, \bold{4}
   7.752    \item pattern matching
   7.753 -    \subitem and \isacommand{recdef}, 45
   7.754 +    \subitem and \isacommand{recdef}, 47
   7.755    \item patterns
   7.756 -    \subitem higher-order, \bold{157}
   7.757 -  \item PDL, 102--104
   7.758 -  \item \isacommand {pr} (command), 14, 84
   7.759 -  \item \isacommand {prefer} (command), 14, 84
   7.760 +    \subitem higher-order, \bold{165}
   7.761 +  \item PDL, 108--110
   7.762 +  \item \isacommand {pr} (command), 16, 90
   7.763 +  \item \isacommand {prefer} (command), 16, 90
   7.764    \item primitive recursion, \see{recursion, primitive}{1}
   7.765 -  \item \isacommand {primrec} (command), 8, 16, 36--41
   7.766 +  \item \isacommand {primrec} (command), 10, 18, 38--43
   7.767    \item product type, \see{pairs and tuples}{1}
   7.768 -  \item Proof General, \bold{5}
   7.769 -  \item proof state, 10
   7.770 +  \item Proof General, \bold{7}
   7.771 +  \item proof state, 12
   7.772    \item proofs
   7.773 -    \subitem abandoning, \bold{11}
   7.774 -    \subitem examples of failing, 71--73
   7.775 +    \subitem abandoning, \bold{13}
   7.776 +    \subitem examples of failing, 77--79
   7.777    \item protocols
   7.778 -    \subitem security, 175--185
   7.779 +    \subitem security, 183--193
   7.780  
   7.781    \indexspace
   7.782  
   7.783 -  \item quantifiers, 3
   7.784 -    \subitem and inductive definitions, 119--121
   7.785 -    \subitem existential, 66
   7.786 -    \subitem for sets, 92
   7.787 -    \subitem instantiating, 68
   7.788 -    \subitem universal, 63--66
   7.789 +  \item quantifiers, 5
   7.790 +    \subitem and inductive definitions, 125--127
   7.791 +    \subitem existential, 72
   7.792 +    \subitem for sets, 98
   7.793 +    \subitem instantiating, 74
   7.794 +    \subitem universal, 69--72
   7.795  
   7.796    \indexspace
   7.797  
   7.798 -  \item \isa {r_into_rtrancl} (theorem), \bold{96}
   7.799 -  \item \isa {r_into_trancl} (theorem), \bold{97}
   7.800 +  \item \isa {r_into_rtrancl} (theorem), \bold{102}
   7.801 +  \item \isa {r_into_trancl} (theorem), \bold{103}
   7.802    \item range
   7.803 -    \subitem of a function, 95
   7.804 -    \subitem of a relation, 96
   7.805 -  \item \isa {range} (symbol), 95
   7.806 -  \item \isa {Range_iff} (theorem), \bold{96}
   7.807 -  \item \isa {Real} (theory), 137
   7.808 -  \item \isa {real} (type), 136--137
   7.809 -  \item real numbers, 136--137
   7.810 -  \item \isacommand {recdef} (command), 44--50, 98, 158--166
   7.811 -    \subitem and numeric literals, 132
   7.812 -  \item \isa {recdef_cong} (attribute), 162
   7.813 -  \item \isa {recdef_simp} (attribute), 46
   7.814 -  \item \isa {recdef_wf} (attribute), 160
   7.815 -  \item \isacommand {record} (command), 140
   7.816 -  \item \isa {record_split} (method), 143
   7.817 -  \item records, 140--144
   7.818 -    \subitem extensible, 141--142
   7.819 +    \subitem of a function, 101
   7.820 +    \subitem of a relation, 102
   7.821 +  \item \isa {range} (symbol), 101
   7.822 +  \item \isa {Range_iff} (theorem), \bold{102}
   7.823 +  \item \isa {Real} (theory), 145
   7.824 +  \item \isa {real} (type), 144--145
   7.825 +  \item real numbers, 144--145
   7.826 +  \item \isacommand {recdef} (command), 46--52, 104, 166--174
   7.827 +    \subitem and numeric literals, 140
   7.828 +  \item \isa {recdef_cong} (attribute), 170
   7.829 +  \item \isa {recdef_simp} (attribute), 48
   7.830 +  \item \isa {recdef_wf} (attribute), 168
   7.831 +  \item \isacommand {record} (command), 148
   7.832 +  \item \isa {record_split} (method), 151
   7.833 +  \item records, 148--152
   7.834 +    \subitem extensible, 149--150
   7.835    \item recursion
   7.836 -    \subitem guarded, 163
   7.837 -    \subitem primitive, 16
   7.838 -    \subitem well-founded, \bold{159}
   7.839 -  \item recursion induction, 49--50
   7.840 -  \item \isacommand {redo} (command), 14
   7.841 -  \item reflexive and transitive closure, 96--98
   7.842 +    \subitem guarded, 171
   7.843 +    \subitem primitive, 18
   7.844 +    \subitem well-founded, \bold{167}
   7.845 +  \item recursion induction, 51--52
   7.846 +  \item \isacommand {redo} (command), 16
   7.847 +  \item reflexive and transitive closure, 102--104
   7.848    \item reflexive transitive closure
   7.849 -    \subitem defining inductively, 116--119
   7.850 -  \item relations, 95--98
   7.851 -    \subitem well-founded, 98--99
   7.852 -  \item \isa {rename_tac} (method), 66--67
   7.853 -  \item \isa {rev} (constant), 8--12, 32
   7.854 -  \item rewrite rules, \bold{25}
   7.855 -    \subitem permutative, \bold{156}
   7.856 -  \item rewriting, \bold{25}
   7.857 -  \item \isa {rotate_tac} (method), 28
   7.858 -  \item \isa {rtrancl_refl} (theorem), \bold{96}
   7.859 -  \item \isa {rtrancl_trans} (theorem), \bold{96}
   7.860 -  \item rule induction, 112--114
   7.861 -  \item rule inversion, 114--115, 123--124
   7.862 -  \item \isa {rule_format} (attribute), 167
   7.863 -  \item \isa {rule_tac} (method), 60
   7.864 -    \subitem and renaming, 67
   7.865 +    \subitem defining inductively, 122--125
   7.866 +  \item relations, 101--104
   7.867 +    \subitem well-founded, 104--105
   7.868 +  \item \isa {rename_tac} (method), 72--73
   7.869 +  \item \isa {rev} (constant), 10--14, 34
   7.870 +  \item rewrite rules, \bold{27}
   7.871 +    \subitem permutative, \bold{164}
   7.872 +  \item rewriting, \bold{27}
   7.873 +  \item \isa {rotate_tac} (method), 30
   7.874 +  \item \isa {rtrancl_refl} (theorem), \bold{102}
   7.875 +  \item \isa {rtrancl_trans} (theorem), \bold{102}
   7.876 +  \item rule induction, 118--120
   7.877 +  \item rule inversion, 120--121, 129--130
   7.878 +  \item \isa {rule_format} (attribute), 175
   7.879 +  \item \isa {rule_tac} (method), 66
   7.880 +    \subitem and renaming, 73
   7.881  
   7.882    \indexspace
   7.883  
   7.884 -  \item \isa {safe} (method), 75, 76
   7.885 -  \item safe rules, \bold{74}
   7.886 -  \item \isa {set} (type), 2, 89
   7.887 -  \item set comprehensions, 91--92
   7.888 -  \item \isa {set_ext} (theorem), \bold{90}
   7.889 -  \item sets, 89--93
   7.890 -    \subitem finite, 93
   7.891 -    \subitem notation for finite, \bold{91}
   7.892 +  \item \isa {safe} (method), 81, 82
   7.893 +  \item safe rules, \bold{80}
   7.894 +  \item \isa {set} (type), 4, 95
   7.895 +  \item set comprehensions, 97--98
   7.896 +  \item \isa {set_ext} (theorem), \bold{96}
   7.897 +  \item sets, 95--99
   7.898 +    \subitem finite, 99
   7.899 +    \subitem notation for finite, \bold{97}
   7.900    \item settings, \see{flags}{1}
   7.901 -  \item \isa {show_brackets} (flag), 4
   7.902 -  \item \isa {show_types} (flag), 3, 14
   7.903 -  \item \isa {simp} (attribute), 9, 26
   7.904 -  \item \isa {simp} (method), \bold{26}
   7.905 -  \item \isa {simp} del (attribute), 26
   7.906 -  \item \isa {simp_all} (method), 26, 35
   7.907 -  \item simplification, 25--31, 155--158
   7.908 -    \subitem of \isa{let}-expressions, 29
   7.909 -    \subitem with definitions, 28
   7.910 -    \subitem with/of assumptions, 27
   7.911 -  \item simplification rule, 157--158
   7.912 -  \item simplification rules, 26
   7.913 -    \subitem adding and deleting, 27
   7.914 -  \item \isa {simplified} (attribute), 77, 80
   7.915 -  \item \isa {size} (constant), 15
   7.916 -  \item \isa {snd} (constant), 22
   7.917 -  \item \isa {SOME} (symbol), 70
   7.918 -  \item \texttt {SOME}, \bold{187}
   7.919 -  \item \isa {Some} (constant), \bold{22}
   7.920 -  \item \isa {some_equality} (theorem), \bold{70}
   7.921 -  \item \isa {someI} (theorem), \bold{70}
   7.922 -  \item \isa {someI2} (theorem), \bold{70}
   7.923 -  \item \isa {someI_ex} (theorem), \bold{71}
   7.924 -  \item sorts, 150
   7.925 -  \item \isa {spec} (theorem), \bold{64}
   7.926 -  \item \isa {split} (attribute), 30
   7.927 -  \item \isa {split} (constant), 137
   7.928 -  \item \isa {split} (method), 29, 138
   7.929 -  \item \isa {split} (modifier), 30
   7.930 -  \item split rule, \bold{30}
   7.931 -  \item \isa {split_if} (theorem), 30
   7.932 -  \item \isa {split_if_asm} (theorem), 30
   7.933 -  \item \isa {ssubst} (theorem), \bold{61}
   7.934 +  \item \isa {show_brackets} (flag), 6
   7.935 +  \item \isa {show_types} (flag), 5, 16
   7.936 +  \item \isa {simp} (attribute), 11, 28
   7.937 +  \item \isa {simp} (method), \bold{28}
   7.938 +  \item \isa {simp} del (attribute), 28
   7.939 +  \item \isa {simp_all} (method), 28, 37
   7.940 +  \item simplification, 27--33, 163--166
   7.941 +    \subitem of \isa{let}-expressions, 31
   7.942 +    \subitem with definitions, 30
   7.943 +    \subitem with/of assumptions, 29
   7.944 +  \item simplification rule, 165--166
   7.945 +  \item simplification rules, 28
   7.946 +    \subitem adding and deleting, 29
   7.947 +  \item \isa {simplified} (attribute), 83, 86
   7.948 +  \item \isa {size} (constant), 17
   7.949 +  \item \isa {snd} (constant), 24
   7.950 +  \item \isa {SOME} (symbol), 76
   7.951 +  \item \texttt {SOME}, \bold{195}
   7.952 +  \item \isa {Some} (constant), \bold{24}
   7.953 +  \item \isa {some_equality} (theorem), \bold{76}
   7.954 +  \item \isa {someI} (theorem), \bold{76}
   7.955 +  \item \isa {someI2} (theorem), \bold{76}
   7.956 +  \item \isa {someI_ex} (theorem), \bold{77}
   7.957 +  \item sorts, 158
   7.958 +  \item \isa {spec} (theorem), \bold{70}
   7.959 +  \item \isa {split} (attribute), 32
   7.960 +  \item \isa {split} (constant), 145
   7.961 +  \item \isa {split} (method), 31, 146
   7.962 +  \item \isa {split} (modifier), 32
   7.963 +  \item split rule, \bold{32}
   7.964 +  \item \isa {split_if} (theorem), 32
   7.965 +  \item \isa {split_if_asm} (theorem), 32
   7.966 +  \item \isa {ssubst} (theorem), \bold{67}
   7.967    \item structural induction, \see{induction, structural}{1}
   7.968 -  \item subclasses, 144, 148
   7.969 -  \item subgoal numbering, 44
   7.970 -  \item \isa {subgoal_tac} (method), 82
   7.971 -  \item subgoals, 10
   7.972 -  \item subset relation, \bold{90}
   7.973 -  \item \isa {subsetD} (theorem), \bold{90}
   7.974 -  \item \isa {subsetI} (theorem), \bold{90}
   7.975 -  \item \isa {subst} (method), 61
   7.976 -  \item substitution, 61--63
   7.977 -  \item \isa {Suc} (constant), 20
   7.978 -  \item \isa {surj_def} (theorem), \bold{94}
   7.979 -  \item surjections, 94
   7.980 -  \item \isa {sym} (theorem), \bold{78}
   7.981 -  \item syntax, 4, 9
   7.982 -  \item syntax translations, 24
   7.983 +  \item subclasses, 152, 156
   7.984 +  \item subgoal numbering, 46
   7.985 +  \item \isa {subgoal_tac} (method), 88
   7.986 +  \item subgoals, 12
   7.987 +  \item subset relation, \bold{96}
   7.988 +  \item \isa {subsetD} (theorem), \bold{96}
   7.989 +  \item \isa {subsetI} (theorem), \bold{96}
   7.990 +  \item \isa {subst} (method), 67
   7.991 +  \item substitution, 67--69
   7.992 +  \item \isa {Suc} (constant), 22
   7.993 +  \item \isa {surj_def} (theorem), \bold{100}
   7.994 +  \item surjections, 100
   7.995 +  \item \isa {sym} (theorem), \bold{84}
   7.996 +  \item syntax, 6, 11
   7.997 +  \item syntax translations, 26
   7.998  
   7.999    \indexspace
  7.1000  
  7.1001 -  \item tacticals, 83
  7.1002 -  \item tactics, 10
  7.1003 -  \item \isacommand {term} (command), 14
  7.1004 -  \item term rewriting, \bold{25}
  7.1005 +  \item tacticals, 89
  7.1006 +  \item tactics, 12
  7.1007 +  \item \isacommand {term} (command), 16
  7.1008 +  \item term rewriting, \bold{27}
  7.1009    \item termination, \see{functions, total}{1}
  7.1010 -  \item terms, 3
  7.1011 -  \item \isa {THE} (symbol), 69
  7.1012 -  \item \isa {the_equality} (theorem), \bold{69}
  7.1013 -  \item \isa {THEN} (attribute), \bold{78}, 80, 86
  7.1014 -  \item \isacommand {theorem} (command), \bold{9}, 11
  7.1015 -  \item theories, 2
  7.1016 -    \subitem abandoning, \bold{14}
  7.1017 -  \item \isacommand {theory} (command), 14
  7.1018 -  \item theory files, 2
  7.1019 -  \item \isacommand {thm} (command), 14
  7.1020 -  \item \isa {tl} (constant), 15
  7.1021 -  \item \isa {ToyList} example, 7--13
  7.1022 -  \item \isa {trace_simp} (flag), 31
  7.1023 -  \item tracing the simplifier, \bold{31}
  7.1024 -  \item \isa {trancl_trans} (theorem), \bold{97}
  7.1025 -  \item transition systems, 101
  7.1026 -  \item \isacommand {translations} (command), 24
  7.1027 -  \item tries, 41--44
  7.1028 -  \item \isa {True} (constant), 3
  7.1029 +  \item terms, 5
  7.1030 +  \item \isa {THE} (symbol), 75
  7.1031 +  \item \isa {the_equality} (theorem), \bold{75}
  7.1032 +  \item \isa {THEN} (attribute), \bold{84}, 86, 92
  7.1033 +  \item \isacommand {theorem} (command), \bold{11}, 13
  7.1034 +  \item theories, 4
  7.1035 +    \subitem abandoning, \bold{16}
  7.1036 +  \item \isacommand {theory} (command), 16
  7.1037 +  \item theory files, 4
  7.1038 +  \item \isacommand {thm} (command), 16
  7.1039 +  \item \isa {tl} (constant), 17
  7.1040 +  \item \isa {ToyList} example, 9--15
  7.1041 +  \item \isa {trace_simp} (flag), 33
  7.1042 +  \item tracing the simplifier, \bold{33}
  7.1043 +  \item \isa {trancl_trans} (theorem), \bold{103}
  7.1044 +  \item transition systems, 107
  7.1045 +  \item \isacommand {translations} (command), 26
  7.1046 +  \item tries, 43--46
  7.1047 +  \item \isa {True} (constant), 5
  7.1048    \item tuples, \see{pairs and tuples}{1}
  7.1049 -  \item \isacommand {typ} (command), 14
  7.1050 -  \item type constraints, \bold{4}
  7.1051 -  \item type constructors, 2
  7.1052 -  \item type inference, \bold{3}
  7.1053 -  \item type synonyms, 23
  7.1054 -  \item type variables, 3
  7.1055 -  \item \isacommand {typedecl} (command), 101, 150
  7.1056 -  \item \isacommand {typedef} (command), 151--154
  7.1057 -  \item types, 2--3
  7.1058 -    \subitem declaring, 150--151
  7.1059 -    \subitem defining, 151--154
  7.1060 -  \item \isacommand {types} (command), 23
  7.1061 +  \item \isacommand {typ} (command), 16
  7.1062 +  \item type constraints, \bold{6}
  7.1063 +  \item type constructors, 4
  7.1064 +  \item type inference, \bold{5}
  7.1065 +  \item type synonyms, 25
  7.1066 +  \item type variables, 5
  7.1067 +  \item \isacommand {typedecl} (command), 107, 158
  7.1068 +  \item \isacommand {typedef} (command), 159--162
  7.1069 +  \item types, 4--5
  7.1070 +    \subitem declaring, 158--159
  7.1071 +    \subitem defining, 159--162
  7.1072 +  \item \isacommand {types} (command), 25
  7.1073  
  7.1074    \indexspace
  7.1075  
  7.1076 -  \item Ullman, J. D., 129
  7.1077 -  \item \texttt {UN}, \bold{187}
  7.1078 -  \item \texttt {Un}, \bold{187}
  7.1079 -  \item \isa {UN_E} (theorem), \bold{92}
  7.1080 -  \item \isa {UN_I} (theorem), \bold{92}
  7.1081 -  \item \isa {UN_iff} (theorem), \bold{92}
  7.1082 -  \item \isa {Un_subset_iff} (theorem), \bold{90}
  7.1083 -  \item \isacommand {undo} (command), 14
  7.1084 -  \item unification, 60--63
  7.1085 -  \item \isa {UNION} (constant), 93
  7.1086 -  \item \texttt {Union}, \bold{187}
  7.1087 +  \item Ullman, J. D., 135
  7.1088 +  \item \texttt {UN}, \bold{195}
  7.1089 +  \item \texttt {Un}, \bold{195}
  7.1090 +  \item \isa {UN_E} (theorem), \bold{98}
  7.1091 +  \item \isa {UN_I} (theorem), \bold{98}
  7.1092 +  \item \isa {UN_iff} (theorem), \bold{98}
  7.1093 +  \item \isa {Un_subset_iff} (theorem), \bold{96}
  7.1094 +  \item \isacommand {undo} (command), 16
  7.1095 +  \item unification, 66--69
  7.1096 +  \item \isa {UNION} (constant), 99
  7.1097 +  \item \texttt {Union}, \bold{195}
  7.1098    \item union
  7.1099 -    \subitem indexed, 92
  7.1100 -  \item \isa {Union_iff} (theorem), \bold{92}
  7.1101 -  \item \isa {unit} (type), 22
  7.1102 -  \item unknowns, 4, \bold{52}
  7.1103 -  \item unsafe rules, \bold{74}
  7.1104 -  \item updating a function, \bold{93}
  7.1105 +    \subitem indexed, 98
  7.1106 +  \item \isa {Union_iff} (theorem), \bold{98}
  7.1107 +  \item \isa {unit} (type), 24
  7.1108 +  \item unknowns, 6, \bold{58}
  7.1109 +  \item unsafe rules, \bold{80}
  7.1110 +  \item updating a function, \bold{99}
  7.1111  
  7.1112    \indexspace
  7.1113  
  7.1114 -  \item variables, 4--5
  7.1115 -    \subitem schematic, 4
  7.1116 -    \subitem type, 3
  7.1117 -  \item \isa {vimage_def} (theorem), \bold{95}
  7.1118 +  \item variables, 6--7
  7.1119 +    \subitem schematic, 6
  7.1120 +    \subitem type, 5
  7.1121 +  \item \isa {vimage_def} (theorem), \bold{101}
  7.1122  
  7.1123    \indexspace
  7.1124  
  7.1125    \item Wenzel, Markus, vii
  7.1126 -  \item \isa {wf_induct} (theorem), \bold{99}
  7.1127 -  \item \isa {wf_inv_image} (theorem), \bold{99}
  7.1128 -  \item \isa {wf_less_than} (theorem), \bold{98}
  7.1129 -  \item \isa {wf_lex_prod} (theorem), \bold{99}
  7.1130 -  \item \isa {wf_measure} (theorem), \bold{99}
  7.1131 -  \item \isa {wf_subset} (theorem), 160
  7.1132 -  \item \isa {while} (constant), 165
  7.1133 -  \item \isa {While_Combinator} (theory), 165
  7.1134 -  \item \isa {while_rule} (theorem), 165
  7.1135 +  \item \isa {wf_induct} (theorem), \bold{105}
  7.1136 +  \item \isa {wf_inv_image} (theorem), \bold{105}
  7.1137 +  \item \isa {wf_less_than} (theorem), \bold{104}
  7.1138 +  \item \isa {wf_lex_prod} (theorem), \bold{105}
  7.1139 +  \item \isa {wf_measure} (theorem), \bold{105}
  7.1140 +  \item \isa {wf_subset} (theorem), 168
  7.1141 +  \item \isa {while} (constant), 173
  7.1142 +  \item \isa {While_Combinator} (theory), 173
  7.1143 +  \item \isa {while_rule} (theorem), 173
  7.1144  
  7.1145    \indexspace
  7.1146  
  7.1147 -  \item \isa {zadd_ac} (theorems), 135
  7.1148 -  \item \isa {zmult_ac} (theorems), 135
  7.1149 +  \item \isa {zadd_ac} (theorems), 143
  7.1150 +  \item \isa {zmult_ac} (theorems), 143
  7.1151  
  7.1152  \end{theindex}
     8.1 --- a/doc-src/TutorialI/tutorial.tex	Mon Oct 01 14:42:47 2001 +0200
     8.2 +++ b/doc-src/TutorialI/tutorial.tex	Mon Oct 01 14:44:00 2001 +0200
     8.3 @@ -54,15 +54,21 @@
     8.4  
     8.5  \cleardoublepage\pagenumbering{arabic}
     8.6  
     8.7 -\input{basics}
     8.8 +\part{Basic Techniques}  %FIXME rename part to "Basic Concepts" (??)
     8.9 +\input{basics}  %FIXME mmw: rename section, move it before part I (??)
    8.10  \input{fp}
    8.11 +\input{Documents/documents}
    8.12 +
    8.13 +\part{Logic and Sets}
    8.14  \input{Rules/rules}
    8.15  \input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
    8.16  \input{Inductive/inductive}
    8.17 +
    8.18 +\part{Advanced Material}
    8.19  \input{Types/types}
    8.20  \input{Advanced/advanced}
    8.21 -%\chapter{Theory Presentation} Document preparation / Syntax Matters!
    8.22  \input{Protocol/protocol}
    8.23 +
    8.24  %\chapter{Structured Proofs}
    8.25  %\label{ch:Isar}
    8.26  %\chapter{Case Study: UNIX File-System Security}