1.1 --- a/doc-src/TutorialI/Advanced/WFrec.thy Tue May 07 14:28:34 2002 +0200
1.2 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Tue May 07 15:03:50 2002 +0200
1.3 @@ -107,7 +107,7 @@
1.4 text{*\noindent
1.5
1.6 Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a
1.7 -crucial hint to our definition:
1.8 +crucial hint\cmmdx{hints} to our definition:
1.9 *}
1.10 (*<*)
1.11 consts g :: "nat \<Rightarrow> nat"
2.1 --- a/doc-src/TutorialI/Advanced/document/WFrec.tex Tue May 07 14:28:34 2002 +0200
2.2 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Tue May 07 15:03:50 2002 +0200
2.3 @@ -121,7 +121,7 @@
2.4 \noindent
2.5
2.6 Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a
2.7 -crucial hint to our definition:%
2.8 +crucial hint\cmmdx{hints} to our definition:%
2.9 \end{isamarkuptext}%
2.10 \isamarkuptrue%
2.11 \isamarkupfalse%
3.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy Tue May 07 14:28:34 2002 +0200
3.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy Tue May 07 15:03:50 2002 +0200
3.3 @@ -64,7 +64,7 @@
3.4 rules for other higher-order functions on lists are similar. If you get
3.5 into a situation where you need to supply \isacommand{recdef} with new
3.6 congruence rules, you can append a hint after the end of
3.7 -the recursion equations:
3.8 +the recursion equations:\cmmdx{hints}
3.9 *}
3.10 (*<*)
3.11 consts dummy :: "nat => nat"
3.12 @@ -84,8 +84,6 @@
3.13 The @{text cong} and @{text recdef_cong} attributes are
3.14 intentionally kept apart because they control different activities, namely
3.15 simplification and making recursive definitions.
3.16 -% The local @{text cong} in
3.17 -% the hints section of \isacommand{recdef} is merely short for @{text recdef_cong}.
3.18 %The simplifier's congruence rules cannot be used by recdef.
3.19 %For example the weak congruence rules for if and case would prevent
3.20 %recdef from generating sensible termination conditions.
4.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex Tue May 07 14:28:34 2002 +0200
4.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Tue May 07 15:03:50 2002 +0200
4.3 @@ -74,7 +74,7 @@
4.4 rules for other higher-order functions on lists are similar. If you get
4.5 into a situation where you need to supply \isacommand{recdef} with new
4.6 congruence rules, you can append a hint after the end of
4.7 -the recursion equations:%
4.8 +the recursion equations:\cmmdx{hints}%
4.9 \end{isamarkuptext}%
4.10 \isamarkuptrue%
4.11 \isamarkupfalse%
4.12 @@ -92,8 +92,6 @@
4.13 The \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
4.14 intentionally kept apart because they control different activities, namely
4.15 simplification and making recursive definitions.
4.16 -% The local \isa{cong} in
4.17 -% the hints section of \isacommand{recdef} is merely short for \isa{recdef{\isacharunderscore}cong}.
4.18 %The simplifier's congruence rules cannot be used by recdef.
4.19 %For example the weak congruence rules for if and case would prevent
4.20 %recdef from generating sensible termination conditions.%
5.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex Tue May 07 14:28:34 2002 +0200
5.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Tue May 07 15:03:50 2002 +0200
5.3 @@ -45,7 +45,7 @@
5.4 proved). Because \isacommand{recdef}'s termination prover involves
5.5 simplification, we include in our second attempt a hint: the
5.6 \attrdx{recdef_simp} attribute says to use \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} as a
5.7 -simplification rule.%
5.8 +simplification rule.\cmmdx{hints}%
5.9 \end{isamarkuptext}%
5.10 \isamarkuptrue%
5.11 \isamarkupfalse%
6.1 --- a/doc-src/TutorialI/Recdef/termination.thy Tue May 07 14:28:34 2002 +0200
6.2 +++ b/doc-src/TutorialI/Recdef/termination.thy Tue May 07 15:03:50 2002 +0200
6.3 @@ -39,7 +39,7 @@
6.4 proved). Because \isacommand{recdef}'s termination prover involves
6.5 simplification, we include in our second attempt a hint: the
6.6 \attrdx{recdef_simp} attribute says to use @{thm[source]less_Suc_eq_le} as a
6.7 -simplification rule. *}
6.8 +simplification rule.\cmmdx{hints} *}
6.9
6.10 (*<*)global consts qs :: "nat list \<Rightarrow> nat list" (*>*)
6.11 recdef qs "measure length"
7.1 --- a/doc-src/TutorialI/tutorial.ind Tue May 07 14:28:34 2002 +0200
7.2 +++ b/doc-src/TutorialI/tutorial.ind Tue May 07 15:03:50 2002 +0200
7.3 @@ -10,7 +10,7 @@
7.4 \item \ttor, \bold{209}
7.5 \item \texttt{[]}, \bold{9}
7.6 \item \texttt{\#}, \bold{9}
7.7 - \item \texttt{\at}, \bold{10}, \hyperpage{209}
7.8 + \item \texttt{\at}, \bold{10}, 209
7.9 \item \isasymnotin, \bold{209}
7.10 \item \verb$~:$, \bold{209}
7.11 \item \isasymInter, \bold{209}
7.12 @@ -26,110 +26,109 @@
7.13 \item \ttrbr, \bold{209}
7.14 \item \texttt {\%}, \bold{209}
7.15 \item \texttt {;}, \bold{7}
7.16 - \item \isa {()} (constant), \hyperpage{24}
7.17 - \item \isa {+} (tactical), \hyperpage{99}
7.18 + \item \isa {()} (constant), 24
7.19 + \item \isa {+} (tactical), 99
7.20 \item \isa {<*lex*>}, \see{lexicographic product}{1}
7.21 - \item \isa {?} (tactical), \hyperpage{99}
7.22 - \item \texttt{|} (tactical), \hyperpage{99}
7.23 + \item \isa {?} (tactical), 99
7.24 + \item \texttt{|} (tactical), 99
7.25
7.26 \indexspace
7.27
7.28 - \item \isa {0} (constant), \hyperpage{22, 23}, \hyperpage{150}
7.29 - \item \isa {1} (constant), \hyperpage{23}, \hyperpage{150, 151}
7.30 + \item \isa {0} (constant), 22, 23, 150
7.31 + \item \isa {1} (constant), 23, 150, 151
7.32
7.33 \indexspace
7.34
7.35 \item abandoning a proof, \bold{13}
7.36 \item abandoning a theory, \bold{16}
7.37 - \item \isa {abs} (constant), \hyperpage{153}
7.38 + \item \isa {abs} (constant), 153
7.39 \item \texttt {abs}, \bold{209}
7.40 - \item absolute value, \hyperpage{153}
7.41 - \item \isa {add} (modifier), \hyperpage{29}
7.42 - \item \isa {add_ac} (theorems), \hyperpage{152}
7.43 + \item absolute value, 153
7.44 + \item \isa {add} (modifier), 29
7.45 + \item \isa {add_ac} (theorems), 152
7.46 \item \isa {add_assoc} (theorem), \bold{152}
7.47 \item \isa {add_commute} (theorem), \bold{152}
7.48 \item \isa {add_mult_distrib} (theorem), \bold{151}
7.49 \item \texttt {ALL}, \bold{209}
7.50 - \item \isa {All} (constant), \hyperpage{109}
7.51 + \item \isa {All} (constant), 109
7.52 \item \isa {allE} (theorem), \bold{81}
7.53 \item \isa {allI} (theorem), \bold{80}
7.54 \item antiquotation, \bold{61}
7.55 \item append function, 10--14
7.56 - \item \isacommand {apply} (command), \hyperpage{15}
7.57 + \item \isacommand {apply} (command), 15
7.58 \item \isa {arg_cong} (theorem), \bold{96}
7.59 - \item \isa {arith} (method), \hyperpage{23}, \hyperpage{149}
7.60 + \item \isa {arith} (method), 23, 149
7.61 \item arithmetic operations
7.62 - \subitem for \protect\isa{nat}, \hyperpage{23}
7.63 + \subitem for \protect\isa{nat}, 23
7.64 \item \textsc {ascii} symbols, \bold{209}
7.65 - \item Aspinall, David, \hyperpage{viii}
7.66 - \item associative-commutative function, \hyperpage{176}
7.67 - \item \isa {assumption} (method), \hyperpage{69}
7.68 + \item Aspinall, David, viii
7.69 + \item associative-commutative function, 176
7.70 + \item \isa {assumption} (method), 69
7.71 \item assumptions
7.72 - \subitem of subgoal, \hyperpage{12}
7.73 + \subitem of subgoal, 12
7.74 \subitem renaming, 82--83
7.75 \subitem reusing, 83
7.76 - \item \isa {auto} (method), \hyperpage{38}, \hyperpage{92}
7.77 + \item \isa {auto} (method), 38, 92
7.78 \item \isa {axclass}, 164--170
7.79 - \item axiom of choice, \hyperpage{86}
7.80 + \item axiom of choice, 86
7.81 \item axiomatic type classes, 164--170
7.82
7.83 \indexspace
7.84
7.85 - \item \isacommand {back} (command), \hyperpage{78}
7.86 - \item \isa {Ball} (constant), \hyperpage{109}
7.87 + \item \isacommand {back} (command), 78
7.88 + \item \isa {Ball} (constant), 109
7.89 \item \isa {ballI} (theorem), \bold{108}
7.90 - \item \isa {best} (method), \hyperpage{92}
7.91 - \item \isa {Bex} (constant), \hyperpage{109}
7.92 + \item \isa {best} (method), 92
7.93 + \item \isa {Bex} (constant), 109
7.94 \item \isa {bexE} (theorem), \bold{108}
7.95 \item \isa {bexI} (theorem), \bold{108}
7.96 \item \isa {bij_def} (theorem), \bold{110}
7.97 - \item bijections, \hyperpage{110}
7.98 - \item binary trees, \hyperpage{18}
7.99 - \item binomial coefficients, \hyperpage{109}
7.100 - \item bisimulations, \hyperpage{116}
7.101 - \item \isa {blast} (method), 89--90, \hyperpage{92}
7.102 - \item \isa {bool} (type), \hyperpage{4, 5}
7.103 + \item bijections, 110
7.104 + \item binary trees, 18
7.105 + \item binomial coefficients, 109
7.106 + \item bisimulations, 116
7.107 + \item \isa {blast} (method), 89--90, 92
7.108 + \item \isa {bool} (type), 4, 5
7.109 \item boolean expressions example, 20--22
7.110 \item \isa {bspec} (theorem), \bold{108}
7.111 \item \isacommand{by} (command), 73
7.112
7.113 \indexspace
7.114
7.115 - \item \isa {card} (constant), \hyperpage{109}
7.116 + \item \isa {card} (constant), 109
7.117 \item \isa {card_Pow} (theorem), \bold{109}
7.118 \item \isa {card_Un_Int} (theorem), \bold{109}
7.119 - \item cardinality, \hyperpage{109}
7.120 - \item \isa {case} (symbol), \hyperpage{32, 33}
7.121 - \item \isa {case} expressions, \hyperpage{5, 6}, \hyperpage{18}
7.122 - \item case distinctions, \hyperpage{19}
7.123 + \item cardinality, 109
7.124 + \item \isa {case} (symbol), 32, 33
7.125 + \item \isa {case} expressions, 5, 6, 18
7.126 + \item case distinctions, 19
7.127 \item case splits, \bold{31}
7.128 - \item \isa {case_tac} (method), \hyperpage{19}, \hyperpage{101},
7.129 - \hyperpage{157}
7.130 - \item \isa {cases} (method), \hyperpage{162}
7.131 - \item \isacommand {chapter} (command), \hyperpage{59}
7.132 - \item \isa {clarify} (method), \hyperpage{91, 92}
7.133 - \item \isa {clarsimp} (method), \hyperpage{91, 92}
7.134 + \item \isa {case_tac} (method), 19, 101, 157
7.135 + \item \isa {cases} (method), 162
7.136 + \item \isacommand {chapter} (command), 59
7.137 + \item \isa {clarify} (method), 91, 92
7.138 + \item \isa {clarsimp} (method), 91, 92
7.139 \item \isa {classical} (theorem), \bold{73}
7.140 \item coinduction, \bold{116}
7.141 - \item \isa {Collect} (constant), \hyperpage{109}
7.142 + \item \isa {Collect} (constant), 109
7.143 \item compiling expressions example, 36--38
7.144 \item \isa {Compl_iff} (theorem), \bold{106}
7.145 \item complement
7.146 - \subitem of a set, \hyperpage{105}
7.147 + \subitem of a set, 105
7.148 \item composition
7.149 \subitem of functions, \bold{110}
7.150 \subitem of relations, \bold{112}
7.151 \item conclusion
7.152 - \subitem of subgoal, \hyperpage{12}
7.153 + \subitem of subgoal, 12
7.154 \item conditional expressions, \see{\isa{if} expressions}{1}
7.155 - \item conditional simplification rules, \hyperpage{31}
7.156 - \item \isa {cong} (attribute), \hyperpage{176}
7.157 + \item conditional simplification rules, 31
7.158 + \item \isa {cong} (attribute), 176
7.159 \item congruence rules, \bold{175}
7.160 \item \isa {conjE} (theorem), \bold{71}
7.161 \item \isa {conjI} (theorem), \bold{68}
7.162 - \item \isa {Cons} (constant), \hyperpage{9}
7.163 - \item \isacommand {constdefs} (command), \hyperpage{25}
7.164 - \item \isacommand {consts} (command), \hyperpage{10}
7.165 + \item \isa {Cons} (constant), 9
7.166 + \item \isacommand {constdefs} (command), 25
7.167 + \item \isacommand {consts} (command), 10
7.168 \item contrapositives, 73
7.169 \item converse
7.170 \subitem of a relation, \bold{112}
7.171 @@ -138,118 +137,118 @@
7.172
7.173 \indexspace
7.174
7.175 - \item \isacommand {datatype} (command), \hyperpage{9}, 38--43
7.176 + \item \isacommand {datatype} (command), 9, 38--43
7.177 \item datatypes, 17--22
7.178 - \subitem and nested recursion, \hyperpage{40}, \hyperpage{44}
7.179 - \subitem mutually recursive, \hyperpage{38}
7.180 - \subitem nested, \hyperpage{180}
7.181 - \item \isacommand {defer} (command), \hyperpage{16}, \hyperpage{100}
7.182 - \item Definitional Approach, \hyperpage{26}
7.183 + \subitem and nested recursion, 40, 44
7.184 + \subitem mutually recursive, 38
7.185 + \subitem nested, 180
7.186 + \item \isacommand {defer} (command), 16, 100
7.187 + \item Definitional Approach, 26
7.188 \item definitions, \bold{25}
7.189 \subitem unfolding, \bold{30}
7.190 - \item \isacommand {defs} (command), \hyperpage{25}
7.191 - \item \isa {del} (modifier), \hyperpage{29}
7.192 + \item \isacommand {defs} (command), 25
7.193 + \item \isa {del} (modifier), 29
7.194 \item description operators, 85--87
7.195 \item descriptions
7.196 - \subitem definite, \hyperpage{85}
7.197 - \subitem indefinite, \hyperpage{86}
7.198 - \item \isa {dest} (attribute), \hyperpage{102}
7.199 + \subitem definite, 85
7.200 + \subitem indefinite, 86
7.201 + \item \isa {dest} (attribute), 102
7.202 \item destruction rules, 71
7.203 \item \isa {diff_mult_distrib} (theorem), \bold{151}
7.204 \item difference
7.205 \subitem of sets, \bold{106}
7.206 \item \isa {disjCI} (theorem), \bold{74}
7.207 \item \isa {disjE} (theorem), \bold{70}
7.208 - \item \isa {div} (symbol), \hyperpage{23}
7.209 - \item divides relation, \hyperpage{84}, \hyperpage{95}, 101--104,
7.210 - \hyperpage{152}
7.211 + \item \isa {div} (symbol), 23
7.212 + \item divides relation, 84, 95, 101--104, 152
7.213 \item division
7.214 - \subitem by negative numbers, \hyperpage{153}
7.215 - \subitem by zero, \hyperpage{152}
7.216 - \subitem for type \protect\isa{nat}, \hyperpage{151}
7.217 + \subitem by negative numbers, 153
7.218 + \subitem by zero, 152
7.219 + \subitem for type \protect\isa{nat}, 151
7.220 \item documents, \bold{57}
7.221 \item domain
7.222 - \subitem of a relation, \hyperpage{112}
7.223 + \subitem of a relation, 112
7.224 \item \isa {Domain_iff} (theorem), \bold{112}
7.225 - \item \isacommand {done} (command), \hyperpage{13}
7.226 - \item \isa {drule_tac} (method), \hyperpage{76}, \hyperpage{96}
7.227 + \item \isacommand {done} (command), 13
7.228 + \item \isa {drule_tac} (method), 76, 96
7.229 \item \isa {dvd_add} (theorem), \bold{152}
7.230 \item \isa {dvd_anti_sym} (theorem), \bold{152}
7.231 \item \isa {dvd_def} (theorem), \bold{152}
7.232
7.233 \indexspace
7.234
7.235 - \item \isa {elim!} (attribute), \hyperpage{131}
7.236 + \item \isa {elim!} (attribute), 131
7.237 \item elimination rules, 69--70
7.238 - \item \isacommand {end} (command), \hyperpage{14}
7.239 - \item \isa {Eps} (constant), \hyperpage{109}
7.240 - \item equality, \hyperpage{5}
7.241 + \item \isacommand {end} (command), 14
7.242 + \item \isa {Eps} (constant), 109
7.243 + \item equality, 5
7.244 \subitem of functions, \bold{109}
7.245 - \subitem of records, \hyperpage{161}
7.246 + \subitem of records, 161
7.247 \subitem of sets, \bold{106}
7.248 \item \isa {equalityE} (theorem), \bold{106}
7.249 \item \isa {equalityI} (theorem), \bold{106}
7.250 - \item \isa {erule} (method), \hyperpage{70}
7.251 - \item \isa {erule_tac} (method), \hyperpage{76}
7.252 + \item \isa {erule} (method), 70
7.253 + \item \isa {erule_tac} (method), 76
7.254 \item Euclid's algorithm, 101--104
7.255 \item even numbers
7.256 \subitem defining inductively, 127--131
7.257 \item \texttt {EX}, \bold{209}
7.258 - \item \isa {Ex} (constant), \hyperpage{109}
7.259 + \item \isa {Ex} (constant), 109
7.260 \item \isa {exE} (theorem), \bold{82}
7.261 \item \isa {exI} (theorem), \bold{82}
7.262 \item \isa {ext} (theorem), \bold{109}
7.263 - \item \isa {extend} (constant), \hyperpage{163}
7.264 + \item \isa {extend} (constant), 163
7.265 \item extensionality
7.266 \subitem for functions, \bold{109, 110}
7.267 - \subitem for records, \hyperpage{162}
7.268 + \subitem for records, 162
7.269 \subitem for sets, \bold{106}
7.270 \item \ttEXU, \bold{209}
7.271
7.272 \indexspace
7.273
7.274 - \item \isa {False} (constant), \hyperpage{5}
7.275 - \item \isa {fast} (method), \hyperpage{92}, \hyperpage{124}
7.276 - \item Fibonacci function, \hyperpage{47}
7.277 - \item \isa {fields} (constant), \hyperpage{163}
7.278 - \item \isa {finite} (symbol), \hyperpage{109}
7.279 - \item \isa {Finites} (constant), \hyperpage{109}
7.280 + \item \isa {False} (constant), 5
7.281 + \item \isa {fast} (method), 92, 124
7.282 + \item Fibonacci function, 47
7.283 + \item \isa {fields} (constant), 163
7.284 + \item \isa {finite} (symbol), 109
7.285 + \item \isa {Finites} (constant), 109
7.286 \item fixed points, 116
7.287 - \item flags, \hyperpage{5, 6}, \hyperpage{33}
7.288 - \subitem setting and resetting, \hyperpage{5}
7.289 - \item \isa {force} (method), \hyperpage{91, 92}
7.290 + \item flags, 5, 6, 33
7.291 + \subitem setting and resetting, 5
7.292 + \item \isa {force} (method), 91, 92
7.293 \item formal comments, \bold{61}
7.294 \item formal proof documents, \bold{57}
7.295 \item formulae, 5--6
7.296 \item forward proof, 92--98
7.297 \item \isa {frule} (method), 83
7.298 - \item \isa {frule_tac} (method), \hyperpage{76}
7.299 - \item \isa {fst} (constant), \hyperpage{24}
7.300 - \item function types, \hyperpage{5}
7.301 + \item \isa {frule_tac} (method), 76
7.302 + \item \isa {fst} (constant), 24
7.303 + \item function types, 5
7.304 \item functions, 109--111
7.305 - \subitem partial, \hyperpage{182}
7.306 - \subitem total, \hyperpage{11}, 47--52
7.307 - \subitem underdefined, \hyperpage{183}
7.308 + \subitem partial, 182
7.309 + \subitem total, 11, 46--52
7.310 + \subitem underdefined, 183
7.311
7.312 \indexspace
7.313
7.314 \item \isa {gcd} (constant), 93--94, 101--104
7.315 - \item generalizing for induction, \hyperpage{129}
7.316 - \item generalizing induction formulae, \hyperpage{35}
7.317 + \item generalizing for induction, 129
7.318 + \item generalizing induction formulae, 35
7.319 \item Girard, Jean-Yves, \fnote{71}
7.320 - \item Gordon, Mike, \hyperpage{3}
7.321 + \item Gordon, Mike, 3
7.322 \item grammars
7.323 \subitem defining inductively, 140--145
7.324 \item ground terms example, 135--140
7.325
7.326 \indexspace
7.327
7.328 - \item \isa {hd} (constant), \hyperpage{17}, \hyperpage{37}
7.329 - \item \isacommand {header} (command), \hyperpage{59}
7.330 - \item Hilbert's $\varepsilon$-operator, \hyperpage{86}
7.331 - \item HOLCF, \hyperpage{43}
7.332 - \item Hopcroft, J. E., \hyperpage{145}
7.333 - \item \isa {hypreal} (type), \hyperpage{155}
7.334 + \item \isa {hd} (constant), 17, 37
7.335 + \item \isacommand {header} (command), 59
7.336 + \item Hilbert's $\varepsilon$-operator, 86
7.337 + \item \isacommand {hints} (command), 49, 180, 182
7.338 + \item HOLCF, 43
7.339 + \item Hopcroft, J. E., 145
7.340 + \item \isa {hypreal} (type), 155
7.341
7.342 \indexspace
7.343
7.344 @@ -259,12 +258,11 @@
7.345 \subitem qualified, \bold{4}
7.346 \item identity function, \bold{110}
7.347 \item identity relation, \bold{112}
7.348 - \item \isa {if} expressions, \hyperpage{5, 6}
7.349 - \subitem simplification of, \hyperpage{33}
7.350 - \subitem splitting of, \hyperpage{31}, \hyperpage{49}
7.351 - \item if-and-only-if, \hyperpage{6}
7.352 - \item \isa {iff} (attribute), \hyperpage{90}, \hyperpage{102},
7.353 - \hyperpage{130}
7.354 + \item \isa {if} expressions, 5, 6
7.355 + \subitem simplification of, 33
7.356 + \subitem splitting of, 31, 49
7.357 + \item if-and-only-if, 6
7.358 + \item \isa {iff} (attribute), 90, 102, 130
7.359 \item \isa {iffD1} (theorem), \bold{94}
7.360 \item \isa {iffD2} (theorem), \bold{94}
7.361 \item ignored material, \bold{64}
7.362 @@ -275,30 +273,28 @@
7.363 \item \isa {Image_iff} (theorem), \bold{112}
7.364 \item \isa {impI} (theorem), \bold{72}
7.365 \item implication, 72--73
7.366 - \item \isa {ind_cases} (method), \hyperpage{131}
7.367 - \item \isa {induct_tac} (method), \hyperpage{12}, \hyperpage{19},
7.368 - \hyperpage{52}, \hyperpage{190}
7.369 + \item \isa {ind_cases} (method), 131
7.370 + \item \isa {induct_tac} (method), 12, 19, 52, 190
7.371 \item induction, 186--193
7.372 - \subitem complete, \hyperpage{188}
7.373 - \subitem deriving new schemas, \hyperpage{190}
7.374 - \subitem on a term, \hyperpage{187}
7.375 + \subitem complete, 188
7.376 + \subitem deriving new schemas, 190
7.377 + \subitem on a term, 187
7.378 \subitem recursion, 51--52
7.379 - \subitem structural, \hyperpage{19}
7.380 + \subitem structural, 19
7.381 \subitem well-founded, 115
7.382 \item induction heuristics, 34--36
7.383 - \item \isacommand {inductive} (command), \hyperpage{127}
7.384 + \item \isacommand {inductive} (command), 127
7.385 \item inductive definition
7.386 - \subitem simultaneous, \hyperpage{141}
7.387 + \subitem simultaneous, 141
7.388 \item inductive definitions, 127--145
7.389 - \item \isacommand {inductive\_cases} (command), \hyperpage{131},
7.390 - \hyperpage{139}
7.391 - \item infinitely branching trees, \hyperpage{43}
7.392 - \item infix annotations, \hyperpage{53}
7.393 - \item \isacommand{infixr} (annotation), \hyperpage{10}
7.394 + \item \isacommand {inductive\_cases} (command), 131, 139
7.395 + \item infinitely branching trees, 43
7.396 + \item infix annotations, 53
7.397 + \item \isacommand{infixr} (annotation), 10
7.398 \item \isa {inj_on_def} (theorem), \bold{110}
7.399 - \item injections, \hyperpage{110}
7.400 - \item \isa {insert} (constant), \hyperpage{107}
7.401 - \item \isa {insert} (method), \hyperpage{97}, 97, \hyperpage{98}
7.402 + \item injections, 110
7.403 + \item \isa {insert} (constant), 107
7.404 + \item \isa {insert} (method), 97--98
7.405 \item instance, \bold{166}
7.406 \item \texttt {INT}, \bold{209}
7.407 \item \texttt {Int}, \bold{209}
7.408 @@ -307,141 +303,139 @@
7.409 \item \isa {IntD1} (theorem), \bold{105}
7.410 \item \isa {IntD2} (theorem), \bold{105}
7.411 \item integers, 153--154
7.412 - \item \isa {INTER} (constant), \hyperpage{109}
7.413 + \item \isa {INTER} (constant), 109
7.414 \item \texttt {Inter}, \bold{209}
7.415 \item \isa {Inter_iff} (theorem), \bold{108}
7.416 - \item intersection, \hyperpage{105}
7.417 - \subitem indexed, \hyperpage{108}
7.418 + \item intersection, 105
7.419 + \subitem indexed, 108
7.420 \item \isa {IntI} (theorem), \bold{105}
7.421 - \item \isa {intro} (method), \hyperpage{74}
7.422 - \item \isa {intro!} (attribute), \hyperpage{128}
7.423 - \item \isa {intro_classes} (method), \hyperpage{166}
7.424 + \item \isa {intro} (method), 74
7.425 + \item \isa {intro!} (attribute), 128
7.426 + \item \isa {intro_classes} (method), 166
7.427 \item introduction rules, 68--69
7.428 - \item \isa {inv} (constant), \hyperpage{86}
7.429 + \item \isa {inv} (constant), 86
7.430 \item \isa {inv_image_def} (theorem), \bold{115}
7.431 \item inverse
7.432 \subitem of a function, \bold{110}
7.433 \subitem of a relation, \bold{112}
7.434 \item inverse image
7.435 - \subitem of a function, \hyperpage{111}
7.436 - \subitem of a relation, \hyperpage{114}
7.437 - \item \isa {itrev} (constant), \hyperpage{34}
7.438 + \subitem of a function, 111
7.439 + \subitem of a relation, 114
7.440 + \item \isa {itrev} (constant), 34
7.441
7.442 \indexspace
7.443
7.444 - \item \isacommand {kill} (command), \hyperpage{16}
7.445 + \item \isacommand {kill} (command), 16
7.446
7.447 \indexspace
7.448
7.449 - \item $\lambda$ expressions, \hyperpage{5}
7.450 - \item LCF, \hyperpage{43}
7.451 - \item \isa {LEAST} (symbol), \hyperpage{23}, \hyperpage{85}
7.452 + \item $\lambda$ expressions, 5
7.453 + \item LCF, 43
7.454 + \item \isa {LEAST} (symbol), 23, 85
7.455 \item least number operator, \see{\protect\isa{LEAST}}{85}
7.456 - \item Leibniz, Gottfried Wilhelm, \hyperpage{53}
7.457 - \item \isacommand {lemma} (command), \hyperpage{13}
7.458 - \item \isacommand {lemmas} (command), \hyperpage{93}, \hyperpage{102}
7.459 - \item \isa {length} (symbol), \hyperpage{18}
7.460 + \item Leibniz, Gottfried Wilhelm, 53
7.461 + \item \isacommand {lemma} (command), 13
7.462 + \item \isacommand {lemmas} (command), 93, 102
7.463 + \item \isa {length} (symbol), 18
7.464 \item \isa {length_induct}, \bold{190}
7.465 - \item \isa {less_than} (constant), \hyperpage{114}
7.466 + \item \isa {less_than} (constant), 114
7.467 \item \isa {less_than_iff} (theorem), \bold{114}
7.468 - \item \isa {let} expressions, \hyperpage{5, 6}, \hyperpage{31}
7.469 - \item \isa {Let_def} (theorem), \hyperpage{31}
7.470 + \item \isa {let} expressions, 5, 6, 31
7.471 + \item \isa {Let_def} (theorem), 31
7.472 \item \isa {lex_prod_def} (theorem), \bold{115}
7.473 - \item lexicographic product, \bold{115}, \hyperpage{178}
7.474 + \item lexicographic product, \bold{115}, 178
7.475 \item {\texttt{lfp}}
7.476 \subitem applications of, \see{CTL}{116}
7.477 - \item Library, \hyperpage{4}
7.478 - \item linear arithmetic, 22--24, \hyperpage{149}
7.479 - \item \isa {List} (theory), \hyperpage{17}
7.480 - \item \isa {list} (type), \hyperpage{5}, \hyperpage{9},
7.481 - \hyperpage{17}
7.482 - \item \isa {list.split} (theorem), \hyperpage{32}
7.483 + \item Library, 4
7.484 + \item linear arithmetic, 22--24, 149
7.485 + \item \isa {List} (theory), 17
7.486 + \item \isa {list} (type), 5, 9, 17
7.487 + \item \isa {list.split} (theorem), 32
7.488 \item \isa {lists_mono} (theorem), \bold{137}
7.489 \item Lowe, Gavin, 196--197
7.490
7.491 \indexspace
7.492
7.493 - \item \isa {Main} (theory), \hyperpage{4}
7.494 + \item \isa {Main} (theory), 4
7.495 \item major premise, \bold{75}
7.496 - \item \isa {make} (constant), \hyperpage{163}
7.497 + \item \isa {make} (constant), 163
7.498 \item marginal comments, \bold{61}
7.499 \item markup commands, \bold{59}
7.500 - \item \isa {max} (constant), \hyperpage{23, 24}
7.501 - \item measure functions, \hyperpage{47}, \hyperpage{114}
7.502 + \item \isa {max} (constant), 23, 24
7.503 + \item measure functions, 47, 114
7.504 \item \isa {measure_def} (theorem), \bold{115}
7.505 \item meta-logic, \bold{80}
7.506 \item methods, \bold{16}
7.507 - \item \isa {min} (constant), \hyperpage{23, 24}
7.508 + \item \isa {min} (constant), 23, 24
7.509 \item mixfix annotations, \bold{53}
7.510 - \item \isa {mod} (symbol), \hyperpage{23}
7.511 + \item \isa {mod} (symbol), 23
7.512 \item \isa {mod_div_equality} (theorem), \bold{151}
7.513 \item \isa {mod_mult_distrib} (theorem), \bold{151}
7.514 \item model checking example, 116--126
7.515 - \item \emph{modus ponens}, \hyperpage{67}, \hyperpage{72}
7.516 + \item \emph{modus ponens}, 67, 72
7.517 \item \isa {mono_def} (theorem), \bold{116}
7.518 - \item monotone functions, \bold{116}, \hyperpage{139}
7.519 + \item monotone functions, \bold{116}, 139
7.520 \subitem and inductive definitions, 137--138
7.521 - \item \isa {more} (constant), \hyperpage{158}, \hyperpage{160}
7.522 + \item \isa {more} (constant), 158, 160
7.523 \item \isa {mp} (theorem), \bold{72}
7.524 - \item \isa {mult_ac} (theorems), \hyperpage{152}
7.525 + \item \isa {mult_ac} (theorems), 152
7.526 \item multiple inheritance, \bold{169}
7.527 \item multiset ordering, \bold{115}
7.528
7.529 \indexspace
7.530
7.531 - \item \isa {nat} (type), \hyperpage{4}, \hyperpage{22}, 151--153
7.532 - \item \isa {nat_less_induct} (theorem), \hyperpage{188}
7.533 + \item \isa {nat} (type), 4, 22, 151--153
7.534 + \item \isa {nat_less_induct} (theorem), 188
7.535 \item natural deduction, 67--68
7.536 - \item natural numbers, \hyperpage{22}, 151--153
7.537 + \item natural numbers, 22, 151--153
7.538 \item Needham-Schroeder protocol, 195--197
7.539 \item negation, 73--75
7.540 - \item \isa {Nil} (constant), \hyperpage{9}
7.541 - \item \isa {no_asm} (modifier), \hyperpage{29}
7.542 - \item \isa {no_asm_simp} (modifier), \hyperpage{30}
7.543 - \item \isa {no_asm_use} (modifier), \hyperpage{30}
7.544 - \item \isa {no_vars} (attribute), \hyperpage{62}
7.545 - \item non-standard reals, \hyperpage{155}
7.546 + \item \isa {Nil} (constant), 9
7.547 + \item \isa {no_asm} (modifier), 29
7.548 + \item \isa {no_asm_simp} (modifier), 30
7.549 + \item \isa {no_asm_use} (modifier), 30
7.550 + \item \isa {no_vars} (attribute), 62
7.551 + \item non-standard reals, 155
7.552 \item \isa {None} (constant), \bold{24}
7.553 \item \isa {notE} (theorem), \bold{73}
7.554 \item \isa {notI} (theorem), \bold{73}
7.555 \item numbers, 149--155
7.556 \item numeric literals, 150
7.557 - \subitem for type \protect\isa{nat}, \hyperpage{151}
7.558 - \subitem for type \protect\isa{real}, \hyperpage{155}
7.559 + \subitem for type \protect\isa{nat}, 151
7.560 + \subitem for type \protect\isa{real}, 155
7.561
7.562 \indexspace
7.563
7.564 - \item \isa {O} (symbol), \hyperpage{112}
7.565 + \item \isa {O} (symbol), 112
7.566 \item \texttt {o}, \bold{209}
7.567 \item \isa {o_def} (theorem), \bold{110}
7.568 - \item \isa {OF} (attribute), 95--96, \hyperpage{96}
7.569 - \item \isa {of} (attribute), \hyperpage{93}, \hyperpage{96}
7.570 - \item \isa {only} (modifier), \hyperpage{29}
7.571 - \item \isacommand {oops} (command), \hyperpage{13}
7.572 + \item \isa {OF} (attribute), 95--96
7.573 + \item \isa {of} (attribute), 93, 96
7.574 + \item \isa {only} (modifier), 29
7.575 + \item \isacommand {oops} (command), 13
7.576 \item \isa {option} (type), \bold{24}
7.577 \item ordered rewriting, \bold{176}
7.578 - \item overloading, \hyperpage{23}, 165--167
7.579 - \subitem and arithmetic, \hyperpage{150}
7.580 + \item overloading, 23, 165--167
7.581 + \subitem and arithmetic, 150
7.582
7.583 \indexspace
7.584
7.585 - \item pairs and tuples, \hyperpage{24}, 155--158
7.586 + \item pairs and tuples, 24, 155--158
7.587 \item parent theories, \bold{4}
7.588 \item pattern matching
7.589 - \subitem and \isacommand{recdef}, \hyperpage{47}
7.590 + \subitem and \isacommand{recdef}, 47
7.591 \item patterns
7.592 \subitem higher-order, \bold{177}
7.593 \item PDL, 118--120
7.594 - \item \isacommand {pr} (command), \hyperpage{16}, \hyperpage{100}
7.595 - \item \isacommand {prefer} (command), \hyperpage{16}, \hyperpage{100}
7.596 - \item prefix annotation, \hyperpage{55}
7.597 + \item \isacommand {pr} (command), 16, 100
7.598 + \item \isacommand {prefer} (command), 16, 100
7.599 + \item prefix annotation, 55
7.600 \item primitive recursion, \see{recursion, primitive}{1}
7.601 - \item \isacommand {primrec} (command), \hyperpage{10}, \hyperpage{18},
7.602 - \hyperpage{41}, 38--43
7.603 + \item \isacommand {primrec} (command), 10, 18, 38--43
7.604 \item print mode, \bold{55}
7.605 \item product type, \see{pairs and tuples}{1}
7.606 \item Proof General, \bold{7}
7.607 - \item proof state, \hyperpage{12}
7.608 + \item proof state, 12
7.609 \item proofs
7.610 \subitem abandoning, \bold{13}
7.611 \subitem examples of failing, 87--89
7.612 @@ -450,11 +444,11 @@
7.613
7.614 \indexspace
7.615
7.616 - \item quantifiers, \hyperpage{6}
7.617 + \item quantifiers, 6
7.618 \subitem and inductive definitions, 135--137
7.619 \subitem existential, 82
7.620 \subitem for sets, 108
7.621 - \subitem instantiating, \hyperpage{84}
7.622 + \subitem instantiating, 84
7.623 \subitem universal, 79--82
7.624
7.625 \indexspace
7.626 @@ -462,28 +456,27 @@
7.627 \item \isa {r_into_rtrancl} (theorem), \bold{112}
7.628 \item \isa {r_into_trancl} (theorem), \bold{113}
7.629 \item range
7.630 - \subitem of a function, \hyperpage{111}
7.631 - \subitem of a relation, \hyperpage{112}
7.632 - \item \isa {range} (symbol), \hyperpage{111}
7.633 + \subitem of a function, 111
7.634 + \subitem of a relation, 112
7.635 + \item \isa {range} (symbol), 111
7.636 \item \isa {Range_iff} (theorem), \bold{112}
7.637 - \item \isa {Real} (theory), \hyperpage{155}
7.638 + \item \isa {Real} (theory), 155
7.639 \item \isa {real} (type), 154--155
7.640 \item real numbers, 154--155
7.641 - \item \isacommand {recdef} (command), 47--52, \hyperpage{114},
7.642 - 178--186
7.643 - \subitem and numeric literals, \hyperpage{150}
7.644 - \item \isa {recdef_cong} (attribute), \hyperpage{182}
7.645 - \item \isa {recdef_simp} (attribute), \hyperpage{49}
7.646 - \item \isa {recdef_wf} (attribute), \hyperpage{180}
7.647 - \item \isacommand {record} (command), \hyperpage{159}
7.648 + \item \isacommand {recdef} (command), 46--52, 114, 178--186
7.649 + \subitem and numeric literals, 150
7.650 + \item \isa {recdef_cong} (attribute), 182
7.651 + \item \isa {recdef_simp} (attribute), 49
7.652 + \item \isa {recdef_wf} (attribute), 180
7.653 + \item \isacommand {record} (command), 159
7.654 \item records, 158--164
7.655 \subitem extensible, 160--161
7.656 \item recursion
7.657 - \subitem guarded, \hyperpage{183}
7.658 - \subitem primitive, \hyperpage{18}
7.659 + \subitem guarded, 183
7.660 + \subitem primitive, 18
7.661 \subitem well-founded, \bold{179}
7.662 \item recursion induction, 51--52
7.663 - \item \isacommand {redo} (command), \hyperpage{16}
7.664 + \item \isacommand {redo} (command), 16
7.665 \item reflexive and transitive closure, 112--114
7.666 \item reflexive transitive closure
7.667 \subitem defining inductively, 132--135
7.668 @@ -491,168 +484,166 @@
7.669 \item relations, 111--114
7.670 \subitem well-founded, 114--115
7.671 \item \isa {rename_tac} (method), 82--83
7.672 - \item \isa {rev} (constant), \hyperpage{10}, 10--14, \hyperpage{34}
7.673 + \item \isa {rev} (constant), 10--14, 34
7.674 \item rewrite rules, \bold{27}
7.675 \subitem permutative, \bold{176}
7.676 \item rewriting, \bold{27}
7.677 - \item \isa {rotate_tac} (method), \hyperpage{30}
7.678 + \item \isa {rotate_tac} (method), 30
7.679 \item \isa {rtrancl_refl} (theorem), \bold{112}
7.680 \item \isa {rtrancl_trans} (theorem), \bold{112}
7.681 \item rule induction, 128--130
7.682 \item rule inversion, 130--131, 139--140
7.683 - \item \isa {rule_format} (attribute), \hyperpage{187}
7.684 - \item \isa {rule_tac} (method), \hyperpage{76}
7.685 - \subitem and renaming, \hyperpage{83}
7.686 + \item \isa {rule_format} (attribute), 187
7.687 + \item \isa {rule_tac} (method), 76
7.688 + \subitem and renaming, 83
7.689
7.690 \indexspace
7.691
7.692 - \item \isa {safe} (method), \hyperpage{91, 92}
7.693 + \item \isa {safe} (method), 91, 92
7.694 \item safe rules, \bold{90}
7.695 - \item \isacommand {sect} (command), \hyperpage{59}
7.696 - \item \isacommand {section} (command), \hyperpage{59}
7.697 + \item \isacommand {sect} (command), 59
7.698 + \item \isacommand {section} (command), 59
7.699 \item selector
7.700 - \subitem record, \hyperpage{159}
7.701 + \subitem record, 159
7.702 \item session, \bold{58}
7.703 - \item \isa {set} (type), \hyperpage{5}, \hyperpage{105}
7.704 + \item \isa {set} (type), 5, 105
7.705 \item set comprehensions, 107--108
7.706 \item \isa {set_ext} (theorem), \bold{106}
7.707 \item sets, 105--109
7.708 - \subitem finite, \hyperpage{109}
7.709 + \subitem finite, 109
7.710 \subitem notation for finite, \bold{107}
7.711 \item settings, \see{flags}{1}
7.712 - \item \isa {show_brackets} (flag), \hyperpage{6}
7.713 - \item \isa {show_types} (flag), \hyperpage{5}, \hyperpage{16}
7.714 - \item \isa {simp} (attribute), \hyperpage{11}, \hyperpage{28}
7.715 + \item \isa {show_brackets} (flag), 6
7.716 + \item \isa {show_types} (flag), 5, 16
7.717 + \item \isa {simp} (attribute), 11, 28
7.718 \item \isa {simp} (method), \bold{28}
7.719 - \item \isa {simp} del (attribute), \hyperpage{28}
7.720 - \item \isa {simp_all} (method), \hyperpage{29}, \hyperpage{38}
7.721 + \item \isa {simp} del (attribute), 28
7.722 + \item \isa {simp_all} (method), 29, 38
7.723 \item simplification, 27--33, 175--178
7.724 - \subitem of \isa{let}-expressions, \hyperpage{31}
7.725 - \subitem with definitions, \hyperpage{30}
7.726 - \subitem with/of assumptions, \hyperpage{29}
7.727 + \subitem of \isa{let}-expressions, 31
7.728 + \subitem with definitions, 30
7.729 + \subitem with/of assumptions, 29
7.730 \item simplification rule, 177--178
7.731 - \item simplification rules, \hyperpage{28}
7.732 - \subitem adding and deleting, \hyperpage{29}
7.733 - \item \isa {simplified} (attribute), \hyperpage{93}, \hyperpage{96}
7.734 - \item \isa {size} (constant), \hyperpage{17}
7.735 - \item \isa {snd} (constant), \hyperpage{24}
7.736 - \item \isa {SOME} (symbol), \hyperpage{86}
7.737 + \item simplification rules, 28
7.738 + \subitem adding and deleting, 29
7.739 + \item \isa {simplified} (attribute), 93, 96
7.740 + \item \isa {size} (constant), 17
7.741 + \item \isa {snd} (constant), 24
7.742 + \item \isa {SOME} (symbol), 86
7.743 \item \texttt {SOME}, \bold{209}
7.744 \item \isa {Some} (constant), \bold{24}
7.745 \item \isa {some_equality} (theorem), \bold{86}
7.746 \item \isa {someI} (theorem), \bold{86}
7.747 \item \isa {someI2} (theorem), \bold{86}
7.748 \item \isa {someI_ex} (theorem), \bold{87}
7.749 - \item sorts, \hyperpage{170}
7.750 + \item sorts, 170
7.751 \item source comments, \bold{60}
7.752 \item \isa {spec} (theorem), \bold{80}
7.753 - \item \isa {split} (attribute), \hyperpage{32}
7.754 - \item \isa {split} (constant), \hyperpage{156}
7.755 - \item \isa {split} (method), \hyperpage{31}, \hyperpage{156}
7.756 - \item \isa {split} (modifier), \hyperpage{32}
7.757 + \item \isa {split} (attribute), 32
7.758 + \item \isa {split} (constant), 156
7.759 + \item \isa {split} (method), 31, 156
7.760 + \item \isa {split} (modifier), 32
7.761 \item split rule, \bold{32}
7.762 - \item \isa {split_if} (theorem), \hyperpage{32}
7.763 - \item \isa {split_if_asm} (theorem), \hyperpage{32}
7.764 + \item \isa {split_if} (theorem), 32
7.765 + \item \isa {split_if_asm} (theorem), 32
7.766 \item \isa {ssubst} (theorem), \bold{77}
7.767 \item structural induction, \see{induction, structural}{1}
7.768 - \item subclasses, \hyperpage{164}, \hyperpage{169}
7.769 - \item subgoal numbering, \hyperpage{46}
7.770 - \item \isa {subgoal_tac} (method), \hyperpage{98}
7.771 - \item subgoals, \hyperpage{12}
7.772 - \item \isacommand {subsect} (command), \hyperpage{59}
7.773 - \item \isacommand {subsection} (command), \hyperpage{59}
7.774 + \item subclasses, 164, 169
7.775 + \item subgoal numbering, 46
7.776 + \item \isa {subgoal_tac} (method), 98
7.777 + \item subgoals, 12
7.778 + \item \isacommand {subsect} (command), 59
7.779 + \item \isacommand {subsection} (command), 59
7.780 \item subset relation, \bold{106}
7.781 \item \isa {subsetD} (theorem), \bold{106}
7.782 \item \isa {subsetI} (theorem), \bold{106}
7.783 - \item \isa {subst} (method), \hyperpage{77}
7.784 + \item \isa {subst} (method), 77
7.785 \item substitution, 77--79
7.786 - \item \isacommand {subsubsect} (command), \hyperpage{59}
7.787 - \item \isacommand {subsubsection} (command), \hyperpage{59}
7.788 - \item \isa {Suc} (constant), \hyperpage{22}
7.789 + \item \isacommand {subsubsect} (command), 59
7.790 + \item \isacommand {subsubsection} (command), 59
7.791 + \item \isa {Suc} (constant), 22
7.792 \item \isa {surj_def} (theorem), \bold{110}
7.793 - \item surjections, \hyperpage{110}
7.794 + \item surjections, 110
7.795 \item \isa {sym} (theorem), \bold{94}
7.796 \item symbols, \bold{54}
7.797 - \item syntax, \hyperpage{6}, \hyperpage{11}
7.798 - \item \isacommand {syntax} (command), \hyperpage{55}
7.799 - \item syntax (command), \hyperpage{56}
7.800 + \item syntax, 6, 11
7.801 + \item \isacommand {syntax} (command), 55
7.802 + \item syntax (command), 56
7.803 \item syntax translations, \bold{56}
7.804
7.805 \indexspace
7.806
7.807 \item tacticals, 99
7.808 - \item tactics, \hyperpage{12}
7.809 - \item \isacommand {term} (command), \hyperpage{16}
7.810 + \item tactics, 12
7.811 + \item \isacommand {term} (command), 16
7.812 \item term rewriting, \bold{27}
7.813 \item termination, \see{functions, total}{1}
7.814 \item terms, 5
7.815 \item text, \bold{61}
7.816 \item text blocks, \bold{61}
7.817 - \item \isa {THE} (symbol), \hyperpage{85}
7.818 + \item \isa {THE} (symbol), 85
7.819 \item \isa {the_equality} (theorem), \bold{85}
7.820 - \item \isa {THEN} (attribute), \bold{94}, \hyperpage{96},
7.821 - \hyperpage{102}
7.822 - \item \isacommand {theorem} (command), \bold{11}, \hyperpage{13}
7.823 + \item \isa {THEN} (attribute), \bold{94}, 96, 102
7.824 + \item \isacommand {theorem} (command), \bold{11}, 13
7.825 \item theories, 4
7.826 \subitem abandoning, \bold{16}
7.827 - \item \isacommand {theory} (command), \hyperpage{16}
7.828 - \item theory files, \hyperpage{4}
7.829 - \item \isacommand {thm} (command), \hyperpage{16}
7.830 - \item \isa {tl} (constant), \hyperpage{17}
7.831 + \item \isacommand {theory} (command), 16
7.832 + \item theory files, 4
7.833 + \item \isacommand {thm} (command), 16
7.834 + \item \isa {tl} (constant), 17
7.835 \item \isa {ToyList} example, 9--14
7.836 - \item \isa {trace_simp} (flag), \hyperpage{33}
7.837 + \item \isa {trace_simp} (flag), 33
7.838 \item tracing the simplifier, \bold{33}
7.839 \item \isa {trancl_trans} (theorem), \bold{113}
7.840 - \item transition systems, \hyperpage{117}
7.841 - \item \isacommand {translations} (command), \hyperpage{56}
7.842 + \item transition systems, 117
7.843 + \item \isacommand {translations} (command), 56
7.844 \item tries, 44--46
7.845 - \item \isa {True} (constant), \hyperpage{5}
7.846 - \item \isa {truncate} (constant), \hyperpage{163}
7.847 + \item \isa {True} (constant), 5
7.848 + \item \isa {truncate} (constant), 163
7.849 \item tuples, \see{pairs and tuples}{1}
7.850 \item txt, \bold{61}
7.851 - \item \isacommand {typ} (command), \hyperpage{16}
7.852 + \item \isacommand {typ} (command), 16
7.853 \item type constraints, \bold{6}
7.854 - \item type constructors, \hyperpage{5}
7.855 + \item type constructors, 5
7.856 \item type inference, \bold{5}
7.857 - \item type synonyms, \hyperpage{25}
7.858 - \item type variables, \hyperpage{5}
7.859 - \item \isacommand {typedecl} (command), \hyperpage{117},
7.860 - \hyperpage{171}
7.861 + \item type synonyms, 25
7.862 + \item type variables, 5
7.863 + \item \isacommand {typedecl} (command), 117, 171
7.864 \item \isacommand {typedef} (command), 171--174
7.865 \item types, 4--5
7.866 \subitem declaring, 171
7.867 \subitem defining, 171--174
7.868 - \item \isacommand {types} (command), \hyperpage{25}
7.869 + \item \isacommand {types} (command), 25
7.870
7.871 \indexspace
7.872
7.873 - \item Ullman, J. D., \hyperpage{145}
7.874 + \item Ullman, J. D., 145
7.875 \item \texttt {UN}, \bold{209}
7.876 \item \texttt {Un}, \bold{209}
7.877 \item \isa {UN_E} (theorem), \bold{108}
7.878 \item \isa {UN_I} (theorem), \bold{108}
7.879 \item \isa {UN_iff} (theorem), \bold{108}
7.880 \item \isa {Un_subset_iff} (theorem), \bold{106}
7.881 - \item \isacommand {undo} (command), \hyperpage{16}
7.882 + \item \isacommand {undo} (command), 16
7.883 \item \isa {unfold} (method), \bold{31}
7.884 \item unification, 76--79
7.885 - \item \isa {UNION} (constant), \hyperpage{109}
7.886 + \item \isa {UNION} (constant), 109
7.887 \item \texttt {Union}, \bold{209}
7.888 \item union
7.889 - \subitem indexed, \hyperpage{108}
7.890 + \subitem indexed, 108
7.891 \item \isa {Union_iff} (theorem), \bold{108}
7.892 - \item \isa {unit} (type), \hyperpage{24}
7.893 - \item unknowns, \hyperpage{7}, \bold{68}
7.894 + \item \isa {unit} (type), 24
7.895 + \item unknowns, 7, \bold{68}
7.896 \item unsafe rules, \bold{90}
7.897 \item update
7.898 - \subitem record, \hyperpage{159}
7.899 + \subitem record, 159
7.900 \item updating a function, \bold{109}
7.901
7.902 \indexspace
7.903
7.904 \item variables, 7
7.905 - \subitem schematic, \hyperpage{7}
7.906 - \subitem type, \hyperpage{5}
7.907 + \subitem schematic, 7
7.908 + \subitem type, 5
7.909 \item \isa {vimage_def} (theorem), \bold{111}
7.910
7.911 \indexspace
7.912 @@ -662,14 +653,14 @@
7.913 \item \isa {wf_less_than} (theorem), \bold{114}
7.914 \item \isa {wf_lex_prod} (theorem), \bold{115}
7.915 \item \isa {wf_measure} (theorem), \bold{115}
7.916 - \item \isa {wf_subset} (theorem), \hyperpage{180}
7.917 - \item \isa {while} (constant), \hyperpage{185}
7.918 - \item \isa {While_Combinator} (theory), \hyperpage{185}
7.919 - \item \isa {while_rule} (theorem), \hyperpage{185}
7.920 + \item \isa {wf_subset} (theorem), 180
7.921 + \item \isa {while} (constant), 185
7.922 + \item \isa {While_Combinator} (theory), 185
7.923 + \item \isa {while_rule} (theorem), 185
7.924
7.925 \indexspace
7.926
7.927 - \item \isa {zadd_ac} (theorems), \hyperpage{153}
7.928 - \item \isa {zmult_ac} (theorems), \hyperpage{153}
7.929 + \item \isa {zadd_ac} (theorems), 153
7.930 + \item \isa {zmult_ac} (theorems), 153
7.931
7.932 \end{theindex}
8.1 --- a/doc-src/TutorialI/tutorial.sty Tue May 07 14:28:34 2002 +0200
8.2 +++ b/doc-src/TutorialI/tutorial.sty Tue May 07 15:03:50 2002 +0200
8.3 @@ -37,8 +37,8 @@
8.4 \newcommand\thydx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theory)}}
8.5
8.6 \newcommand\attrdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (attribute)}}
8.7 -\newcommand\commdx[1]{\isacommand{#1}\index{#1@\protect\isacommand{#1}
8.8 -(command)}}
8.9 +\newcommand\cmmdx[1]{\index{#1@\protect\isacommand{#1} (command)}}
8.10 +\newcommand\commdx[1]{\isacommand{#1}\index{#1@\protect\isacommand{#1} (command)}}
8.11 \newcommand\methdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (method)}}
8.12 \newcommand\tooldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (tool)}}
8.13 \newcommand\settdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (setting)}}