1.1 --- a/doc-src/Intro/Makefile Fri May 02 16:18:11 1997 +0200
1.2 +++ b/doc-src/Intro/Makefile Fri May 02 16:18:49 1997 +0200
1.3 @@ -7,21 +7,21 @@
1.4
1.5
1.6 FILES = intro.tex foundations.tex getting.tex advanced.tex \
1.7 - ../proof209.sty ../iman.sty ../extra.sty
1.8 + ../proof.sty ../iman.sty ../extra.sty
1.9
1.10 intro.dvi.gz: $(FILES)
1.11 -rm intro.dvi*
1.12 - latex209 intro
1.13 + latex intro
1.14 bibtex intro
1.15 - latex209 intro
1.16 - latex209 intro
1.17 + latex intro
1.18 + latex intro
1.19 ../sedindex intro
1.20 - latex209 intro
1.21 + latex intro
1.22 gzip -f intro.dvi
1.23
1.24 dist: $(FILES)
1.25 -rm intro.dvi*
1.26 - latex209 intro
1.27 - latex209 intro
1.28 + latex intro
1.29 + latex intro
1.30 ../sedindex intro
1.31 - latex209 intro
1.32 + latex intro
2.1 --- a/doc-src/Intro/intro.ind Fri May 02 16:18:11 1997 +0200
2.2 +++ b/doc-src/Intro/intro.ind Fri May 02 16:18:49 1997 +0200
2.3 @@ -1,115 +1,115 @@
2.4 \begin{theindex}
2.5
2.6 - \item {\ptt !!} symbol, 24
2.7 - \subitem in main goal, 44
2.8 - \item {\tt\%} symbol, 24
2.9 - \item {\ptt ::} symbol, 24
2.10 - \item {\ptt ==} symbol, 24
2.11 - \item {\ptt ==>} symbol, 24
2.12 - \item {\ptt =>} symbol, 24
2.13 - \item {\ptt =?=} symbol, 24
2.14 - \item {\ptt [} symbol, 24
2.15 - \item {\ptt [|} symbol, 24
2.16 - \item {\ptt ]} symbol, 24
2.17 - \item {\tt\ttlbrace} symbol, 24
2.18 - \item {\tt\ttrbrace} symbol, 24
2.19 - \item {\ptt |]} symbol, 24
2.20 + \item {\tt !!} symbol, 25
2.21 + \subitem in main goal, 46
2.22 + \item {\tt\%} symbol, 25
2.23 + \item {\tt ::} symbol, 25
2.24 + \item {\tt ==} symbol, 25
2.25 + \item {\tt ==>} symbol, 25
2.26 + \item {\tt =>} symbol, 25
2.27 + \item {\tt =?=} symbol, 25
2.28 + \item {\tt [} symbol, 25
2.29 + \item {\tt [|} symbol, 25
2.30 + \item {\tt ]} symbol, 25
2.31 + \item {\tt\ttlbrace} symbol, 25
2.32 + \item {\tt\ttrbrace} symbol, 25
2.33 + \item {\tt |]} symbol, 25
2.34
2.35 \indexspace
2.36
2.37 - \item {\ptt allI} theorem, 35
2.38 + \item {\tt allI} theorem, 37
2.39 \item arities
2.40 - \subitem declaring, 4, \bold{47}
2.41 - \item {\ptt asm_simp_tac}, 57
2.42 - \item {\ptt assume_tac}, 28, 30, 35, 44
2.43 + \subitem declaring, 4, \bold{49}
2.44 + \item {\tt asm_simp_tac}, 60
2.45 + \item {\tt assume_tac}, 29, 31, 37, 47
2.46 \item assumptions
2.47 - \subitem deleting, 19
2.48 + \subitem deleting, 20
2.49 \subitem discharge of, 7
2.50 - \subitem lifting over, 13
2.51 - \subitem of main goal, 39
2.52 - \subitem use of, 16, 27
2.53 + \subitem lifting over, 14
2.54 + \subitem of main goal, 41
2.55 + \subitem use of, 16, 28
2.56 \item axioms
2.57 - \subitem Peano, 52
2.58 + \subitem Peano, 54
2.59
2.60 \indexspace
2.61
2.62 - \item {\ptt ba}, 29
2.63 - \item {\ptt back}, 55, 56, 59
2.64 + \item {\tt ba}, 30
2.65 + \item {\tt back}, 59, 62
2.66 \item backtracking
2.67 - \subitem Prolog style, 59
2.68 - \item {\ptt bd}, 29
2.69 - \item {\ptt be}, 29
2.70 - \item {\ptt br}, 29
2.71 - \item {\ptt by}, 29
2.72 + \subitem Prolog style, 62
2.73 + \item {\tt bd}, 30
2.74 + \item {\tt be}, 30
2.75 + \item {\tt br}, 30
2.76 + \item {\tt by}, 30
2.77
2.78 \indexspace
2.79
2.80 - \item {\ptt choplev}, 34, 35, 61
2.81 + \item {\tt choplev}, 36, 37, 64
2.82 \item classes, 3
2.83 - \subitem built-in, \bold{24}
2.84 - \item classical reasoner, 37
2.85 - \item {\ptt conjunct1} theorem, 26
2.86 + \subitem built-in, \bold{25}
2.87 + \item classical reasoner, 39
2.88 + \item {\tt conjunct1} theorem, 27
2.89 \item constants, 1
2.90 \subitem clashes with variables, 9
2.91 - \subitem declaring, \bold{46}
2.92 - \subitem overloaded, 51
2.93 + \subitem declaring, \bold{48}
2.94 + \subitem overloaded, 53
2.95 \subitem polymorphic, 3
2.96
2.97 \indexspace
2.98
2.99 - \item definitions, 5, \bold{46}
2.100 - \subitem and derived rules, 41--44
2.101 - \item {\ptt DEPTH_FIRST}, 60
2.102 - \item destruct-resolution, 21, 29
2.103 - \item {\ptt disjE} theorem, 30
2.104 - \item {\ptt dres_inst_tac}, 54
2.105 - \item {\ptt dresolve_tac}, 29, 31, 36
2.106 + \item definitions, 6, \bold{48}
2.107 + \subitem and derived rules, 43--46
2.108 + \item {\tt DEPTH_FIRST}, 64
2.109 + \item destruct-resolution, 22, 30
2.110 + \item {\tt disjE} theorem, 31
2.111 + \item {\tt dres_inst_tac}, 57
2.112 + \item {\tt dresolve_tac}, 30, 32, 38
2.113
2.114 \indexspace
2.115
2.116 - \item eigenvariables, \see{parameters}{7}
2.117 - \item elim-resolution, \bold{19}, 28
2.118 + \item eigenvariables, \see{parameters}{8}
2.119 + \item elim-resolution, \bold{20}, 30
2.120 \item equality
2.121 \subitem polymorphic, 3
2.122 - \item {\ptt eres_inst_tac}, 54
2.123 - \item {\ptt eresolve_tac}, 28, 31, 36, 44
2.124 + \item {\tt eres_inst_tac}, 57
2.125 + \item {\tt eresolve_tac}, 30, 32, 38, 47
2.126 \item examples
2.127 - \subitem of deriving rules, 39
2.128 - \subitem of induction, 54, 55
2.129 - \subitem of simplification, 56
2.130 - \subitem of tacticals, 35
2.131 - \subitem of theories, 46, 48--53, 58
2.132 - \subitem propositional, 16, 29, 31
2.133 - \subitem with quantifiers, 17, 32, 33, 36
2.134 - \item {\ptt exE} theorem, 36
2.135 + \subitem of deriving rules, 41
2.136 + \subitem of induction, 57, 58
2.137 + \subitem of simplification, 59
2.138 + \subitem of tacticals, 37
2.139 + \subitem of theories, 48, 50--55, 61
2.140 + \subitem propositional, 17, 31, 32
2.141 + \subitem with quantifiers, 18, 33, 35, 37
2.142 + \item {\tt exE} theorem, 38
2.143
2.144 \indexspace
2.145
2.146 - \item {\ptt FalseE} theorem, 43
2.147 - \item {\ptt fast_tac}, 37
2.148 + \item {\tt FalseE} theorem, 45
2.149 + \item {\tt fast_tac}, 39
2.150 \item first-order logic, 1
2.151 - \item flex-flex constraints, 5, 24, \bold{27}
2.152 - \item {\ptt flexflex_rule}, 27
2.153 - \item forward proof, 20, 23--29
2.154 - \item {\ptt fun} type, 1, 4
2.155 - \item function applications, 1, 7
2.156 + \item flex-flex constraints, 6, 25, \bold{28}
2.157 + \item {\tt flexflex_rule}, 28
2.158 + \item forward proof, 21, 24--30
2.159 + \item {\tt fun} type, 1, 4
2.160 + \item function applications, 1, 8
2.161
2.162 \indexspace
2.163
2.164 - \item {\ptt goal}, 29, 39, 44
2.165 - \item {\ptt goalw}, 42--44
2.166 + \item {\tt goal}, 30, 41, 46
2.167 + \item {\tt goalw}, 44--46
2.168
2.169 \indexspace
2.170
2.171 - \item {\ptt has_fewer_prems}, 61
2.172 + \item {\tt has_fewer_prems}, 64
2.173 \item higher-order logic, 4
2.174
2.175 \indexspace
2.176
2.177 - \item identifiers, 23
2.178 - \item {\ptt impI} theorem, 30, 42
2.179 - \item infixes, 49
2.180 - \item instantiation, 54--57
2.181 + \item identifiers, 24
2.182 + \item {\tt impI} theorem, 31, 44
2.183 + \item infixes, 52
2.184 + \item instantiation, 57--60
2.185 \item Isabelle
2.186 \subitem object-logics supported, i
2.187 \subitem overview, i
2.188 @@ -117,149 +117,149 @@
2.189
2.190 \indexspace
2.191
2.192 - \item $\lambda$-abstractions, 1, 7, 24
2.193 + \item $\lambda$-abstractions, 1, 8, 25
2.194 \item $\lambda$-calculus, 1
2.195 \item LCF, i
2.196 - \item LCF system, 15, 25
2.197 - \item level of a proof, 29
2.198 - \item lifting, \bold{13}
2.199 - \item {\ptt logic} class, 3, 6, 24
2.200 + \item LCF system, 15, 26
2.201 + \item level of a proof, 31
2.202 + \item lifting, \bold{14}
2.203 + \item {\tt logic} class, 3, 6, 25
2.204
2.205 \indexspace
2.206
2.207 - \item major premise, \bold{20}
2.208 - \item {\ptt Match} exception, 40
2.209 + \item major premise, \bold{21}
2.210 + \item {\tt Match} exception, 42
2.211 \item meta-assumptions
2.212 - \subitem syntax of, 21
2.213 - \item meta-equality, \bold{5}, 24
2.214 - \item meta-implication, \bold{5}, 6, 24
2.215 - \item meta-quantifiers, \bold{5}, 7, 24
2.216 - \item meta-rewriting, 41
2.217 - \item mixfix declarations, 49, 50, 53
2.218 + \subitem syntax of, 22
2.219 + \item meta-equality, \bold{5}, 25
2.220 + \item meta-implication, \bold{5}, 7, 25
2.221 + \item meta-quantifiers, \bold{5}, 8, 25
2.222 + \item meta-rewriting, 43
2.223 + \item mixfix declarations, 52, 53, 56
2.224 \item ML, i
2.225 - \item {\ptt ML} section, 45
2.226 - \item {\ptt mp} theorem, 26
2.227 + \item {\tt ML} section, 47
2.228 + \item {\tt mp} theorem, 27
2.229
2.230 \indexspace
2.231
2.232 - \item {\ptt Nat} theory, 53
2.233 - \item {\ptt nat} type, 1, 3
2.234 - \item {\ptt not_def} theorem, 42
2.235 - \item {\ptt notE} theorem, \bold{43}, 55
2.236 - \item {\ptt notI} theorem, \bold{42}, 55
2.237 + \item {\tt Nat} theory, 55
2.238 + \item {\tt nat} type, 1, 3
2.239 + \item {\tt not_def} theorem, 44
2.240 + \item {\tt notE} theorem, \bold{45}, 58
2.241 + \item {\tt notI} theorem, \bold{44}, 58
2.242
2.243 \indexspace
2.244
2.245 - \item {\ptt o} type, 1, 4
2.246 - \item {\ptt ORELSE}, 35
2.247 - \item overloading, \bold{4}, 51
2.248 + \item {\tt o} type, 1, 4
2.249 + \item {\tt ORELSE}, 37
2.250 + \item overloading, \bold{4}, 53
2.251
2.252 \indexspace
2.253
2.254 - \item parameters, \bold{7}, 32
2.255 - \subitem lifting over, 14
2.256 - \item {\ptt Prolog} theory, 58
2.257 - \item Prolog interpreter, \bold{57}
2.258 - \item proof state, 15
2.259 + \item parameters, \bold{8}, 33
2.260 + \subitem lifting over, 15
2.261 + \item {\tt Prolog} theory, 61
2.262 + \item Prolog interpreter, \bold{60}
2.263 + \item proof state, 16
2.264 \item proofs
2.265 - \subitem commands for, 29
2.266 - \item {\ptt PROP} symbol, 25
2.267 - \item {\ptt prop} type, 6, 24
2.268 - \item {\ptt prth}, 26
2.269 - \item {\ptt prthq}, 26, 27
2.270 - \item {\ptt prths}, 26
2.271 - \item {\ptt Pure} theory, 45
2.272 + \subitem commands for, 30
2.273 + \item {\tt PROP} symbol, 26
2.274 + \item {\tt prop} type, 6, 25, 26
2.275 + \item {\tt prth}, 27
2.276 + \item {\tt prthq}, 27, 28
2.277 + \item {\tt prths}, 27
2.278 + \item {\tt Pure} theory, 47
2.279
2.280 \indexspace
2.281
2.282 - \item quantifiers, 5, 7, 32
2.283 + \item quantifiers, 5, 8, 33
2.284
2.285 \indexspace
2.286
2.287 - \item {\ptt read_instantiate}, 28
2.288 - \item {\ptt refl} theorem, 28
2.289 - \item {\ptt REPEAT}, 31, 36, 59, 60
2.290 - \item {\ptt res_inst_tac}, 54, 56
2.291 - \item reserved words, 23
2.292 - \item resolution, 10, \bold{11}
2.293 + \item {\tt read_instantiate}, 29
2.294 + \item {\tt refl} theorem, 29
2.295 + \item {\tt REPEAT}, 33, 37, 62, 64
2.296 + \item {\tt res_inst_tac}, 57, 60
2.297 + \item reserved words, 24
2.298 + \item resolution, 10, \bold{12}
2.299 \subitem in backward proof, 15
2.300 - \subitem with instantiation, 54
2.301 - \item {\ptt resolve_tac}, 28, 30, 43, 55
2.302 - \item {\ptt result}, 29, 40, 44
2.303 - \item {\ptt rewrite_goals_tac}, 42
2.304 - \item {\ptt rewrite_rule}, 43
2.305 - \item {\ptt RL}, 27, 28
2.306 - \item {\ptt RLN}, 27
2.307 - \item {\ptt RS}, 26, 27, 44
2.308 - \item {\ptt RSN}, 26, 27
2.309 + \subitem with instantiation, 57
2.310 + \item {\tt resolve_tac}, 30, 31, 46, 58
2.311 + \item {\tt result}, 30, 42, 46
2.312 + \item {\tt rewrite_goals_tac}, 44
2.313 + \item {\tt rewrite_rule}, 45, 46
2.314 + \item {\tt RL}, 29
2.315 + \item {\tt RLN}, 29
2.316 + \item {\tt RS}, 27, 29, 46
2.317 + \item {\tt RSN}, 27, 29
2.318 \item rules
2.319 - \subitem declaring, 46
2.320 - \subitem derived, 12, \bold{21}, 39, 41
2.321 - \subitem destruction, 20
2.322 - \subitem elimination, 20
2.323 + \subitem declaring, 48
2.324 + \subitem derived, 13, \bold{22}, 41, 43
2.325 + \subitem destruction, 21
2.326 + \subitem elimination, 21
2.327 \subitem propositional, 6
2.328 - \subitem quantifier, 7
2.329 + \subitem quantifier, 8
2.330
2.331 \indexspace
2.332
2.333 \item search
2.334 - \subitem depth-first, 60
2.335 - \item signatures, \bold{8}
2.336 - \item {\ptt simp_tac}, 57
2.337 - \item simplification, 56
2.338 - \item simplification sets, 56
2.339 - \item sort constraints, 24
2.340 - \item sorts, \bold{4}
2.341 - \item {\ptt spec} theorem, 26, 34, 35
2.342 - \item {\ptt standard}, 26
2.343 - \item substitution, \bold{7}
2.344 - \item {\ptt Suc_inject}, 55
2.345 - \item {\ptt Suc_neq_0}, 55
2.346 + \subitem depth-first, 63
2.347 + \item signatures, \bold{9}
2.348 + \item {\tt simp_tac}, 60
2.349 + \item simplification, 59
2.350 + \item simplification sets, 59
2.351 + \item sort constraints, 25
2.352 + \item sorts, \bold{5}
2.353 + \item {\tt spec} theorem, 28, 36, 37
2.354 + \item {\tt standard}, 27
2.355 + \item substitution, \bold{8}
2.356 + \item {\tt Suc_inject}, 58
2.357 + \item {\tt Suc_neq_0}, 58
2.358 \item syntax
2.359 - \subitem of types and terms, 24
2.360 + \subitem of types and terms, 25
2.361
2.362 \indexspace
2.363
2.364 - \item tacticals, \bold{18}, 35
2.365 - \item tactics, \bold{18}
2.366 - \subitem assumption, 28
2.367 - \subitem resolution, 28
2.368 - \item {\ptt term} class, 3
2.369 + \item tacticals, \bold{19}, 37
2.370 + \item tactics, \bold{19}
2.371 + \subitem assumption, 29
2.372 + \subitem resolution, 30
2.373 + \item {\tt term} class, 3
2.374 \item terms
2.375 - \subitem syntax of, 1, \bold{24}
2.376 + \subitem syntax of, 1, \bold{25}
2.377 \item theorems
2.378 - \subitem basic operations on, \bold{25}
2.379 - \subitem printing of, 25
2.380 - \item theories, \bold{8}
2.381 - \subitem defining, 44--54
2.382 - \item {\ptt thm} ML type, 25
2.383 - \item {\ptt topthm}, 40
2.384 - \item {\ptt Trueprop} constant, 6, 24
2.385 - \item type constraints, 24
2.386 + \subitem basic operations on, \bold{26}
2.387 + \subitem printing of, 27
2.388 + \item theories, \bold{9}
2.389 + \subitem defining, 47--57
2.390 + \item {\tt thm} ML type, 26
2.391 + \item {\tt topthm}, 42
2.392 + \item {\tt Trueprop} constant, 6, 7, 25
2.393 + \item type constraints, 25
2.394 \item type constructors, 1
2.395 - \item type identifiers, 23
2.396 - \item type synonyms, \bold{49}
2.397 + \item type identifiers, 24
2.398 + \item type synonyms, \bold{51}
2.399 \item types
2.400 - \subitem declaring, \bold{47}
2.401 + \subitem declaring, \bold{49}
2.402 \subitem function, 1
2.403 \subitem higher, \bold{5}
2.404 \subitem polymorphic, \bold{3}
2.405 \subitem simple, \bold{1}
2.406 - \subitem syntax of, 1, \bold{24}
2.407 + \subitem syntax of, 1, \bold{25}
2.408
2.409 \indexspace
2.410
2.411 - \item {\ptt undo}, 29
2.412 + \item {\tt undo}, 30
2.413 \item unification
2.414 - \subitem higher-order, \bold{10}, 55
2.415 + \subitem higher-order, \bold{11}, 58
2.416 \subitem incompleteness of, 11
2.417 - \item unknowns, 9, 23, 32
2.418 - \subitem function, \bold{11}, 27, 32
2.419 - \item {\ptt use_thy}, \bold{45}
2.420 + \item unknowns, 10, 24, 33
2.421 + \subitem function, \bold{11}, 28, 33
2.422 + \item {\tt use_thy}, \bold{47}
2.423
2.424 \indexspace
2.425
2.426 \item variables
2.427 - \subitem bound, 7
2.428 + \subitem bound, 8
2.429
2.430 \end{theindex}
3.1 --- a/doc-src/Intro/intro.tex Fri May 02 16:18:11 1997 +0200
3.2 +++ b/doc-src/Intro/intro.tex Fri May 02 16:18:49 1997 +0200
3.3 @@ -1,6 +1,8 @@
3.4 -\documentstyle[a4,12pt]{article}
3.5 +\documentclass[12pt]{article}
3.6 +\usepackage{a4}
3.7 +
3.8 \makeatletter
3.9 -\input{../proof209.sty}
3.10 +\input{../proof.sty}
3.11 \input{../iman.sty}
3.12 \input{../extra.sty}
3.13 \makeatother
4.1 --- a/doc-src/Logics/CTT.tex Fri May 02 16:18:11 1997 +0200
4.2 +++ b/doc-src/Logics/CTT.tex Fri May 02 16:18:49 1997 +0200
4.3 @@ -696,7 +696,7 @@
4.4 \tdx{diff_succ_succ} [| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N
4.5 \tdx{diff_self_eq_0} a:N ==> a - a = 0 : N
4.6 \tdx{add_inverse_diff} [| a:N; b:N; b-a=0 : N |] ==> b #+ (a-b) = a : N
4.7 -\caption{The theory of arithmetic} \label{ctt-arith}
4.8 +\caption{The theory of arithmetic} \label{ctt_arith}
4.9 \end{ttbox}
4.10 \end{figure}
4.11
4.12 @@ -706,7 +706,7 @@
4.13 properties of addition, multiplication, subtraction, division, and
4.14 remainder, culminating in the theorem
4.15 \[ a \bmod b + (a/b)\times b = a. \]
4.16 -Figure~\ref{ctt-arith} presents the definitions and some of the key
4.17 +Figure~\ref{ctt_arith} presents the definitions and some of the key
4.18 theorems, including commutative, distributive, and associative laws.
4.19
4.20 The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod'
5.1 --- a/doc-src/Logics/Makefile Fri May 02 16:18:11 1997 +0200
5.2 +++ b/doc-src/Logics/Makefile Fri May 02 16:18:49 1997 +0200
5.3 @@ -7,22 +7,22 @@
5.4
5.5
5.6 FILES = logics.tex intro.tex FOL.tex ZF.tex HOL.tex LK.tex CTT.tex\
5.7 - ../rail.sty ../proof209.sty ../iman.sty ../extra.sty
5.8 + ../rail.sty ../proof.sty ../iman.sty ../extra.sty
5.9
5.10 logics.dvi.gz: $(FILES)
5.11 -rm logics.dvi*
5.12 - latex209 logics
5.13 + latex logics
5.14 rail logics
5.15 bibtex logics
5.16 - latex209 logics
5.17 - latex209 logics
5.18 + latex logics
5.19 + latex logics
5.20 ../sedindex logics
5.21 - latex209 logics
5.22 + latex logics
5.23 gzip -f logics.dvi
5.24
5.25 dist: $(FILES)
5.26 -rm logics.dvi*
5.27 - latex209 logics
5.28 - latex209 logics
5.29 + latex logics
5.30 + latex logics
5.31 ../sedindex logics
5.32 - latex209 logics
5.33 + latex logics
6.1 --- a/doc-src/Logics/logics.ind Fri May 02 16:18:11 1997 +0200
6.2 +++ b/doc-src/Logics/logics.ind Fri May 02 16:18:49 1997 +0200
6.3 @@ -1,974 +1,939 @@
6.4 \begin{theindex}
6.5
6.6 - \item {\ptt !} symbol, 59, 61, 67, 69
6.7 - \item {\tt[]} symbol, 80
6.8 - \item {\tt\#} symbol, 80
6.9 - \item {\tt\#*} symbol, 46, 122
6.10 - \item {\tt\#+} symbol, 46, 122
6.11 + \item {\tt !} symbol, 58, 60, 66, 68
6.12 + \item {\tt[]} symbol, 79
6.13 + \item {\tt\#} symbol, 79
6.14 + \item {\tt\#*} symbol, 46, 121
6.15 + \item {\tt\#+} symbol, 46, 121
6.16 \item {\tt\#-} symbol, 46
6.17 - \item {\tt\&} symbol, 6, 59, 99
6.18 - \item {\ptt *} symbol, 25, 60, 78, 113
6.19 - \item {\ptt *} type, 75
6.20 - \item {\ptt +} symbol, 42, 60, 78, 113
6.21 - \item {\ptt +} type, 75
6.22 - \item {\ptt -} symbol, 24, 60, 78, 122
6.23 - \item {\ptt -->} symbol, 6, 59, 99, 113
6.24 - \item {\ptt ->} symbol, 25
6.25 - \item {\ptt -``} symbol, 24
6.26 - \item {\ptt :} symbol, 24, 66
6.27 - \item {\ptt <} symbol, 78
6.28 - \item {\ptt <->} symbol, 6, 99
6.29 - \item {\ptt <=} symbol, 24, 66
6.30 - \item {\ptt =} symbol, 6, 59, 99, 113
6.31 - \item {\ptt ?} symbol, 59, 61, 67, 69
6.32 - \item {\ptt ?!} symbol, 59
6.33 - \item {\tt\at} symbol, 59, 80
6.34 - \item {\ptt `} symbol, 24, 113
6.35 - \item {\ptt ``} symbol, 24, 66
6.36 - \item \verb'{}' symbol, 66
6.37 - \item {\ptt |} symbol, 6, 59, 99
6.38 - \item {\ptt |-|} symbol, 122
6.39 + \item {\tt\&} symbol, 6, 58, 98
6.40 + \item {\tt *} symbol, 25, 59, 76, 112
6.41 + \item {\tt *} type, 74
6.42 + \item {\tt +} symbol, 42, 59, 76, 112
6.43 + \item {\tt +} type, 74
6.44 + \item {\tt -} symbol, 24, 59, 76, 121
6.45 + \item {\tt -->} symbol, 6, 58, 98, 112
6.46 + \item {\tt ->} symbol, 25
6.47 + \item {\tt -``} symbol, 24
6.48 + \item {\tt :} symbol, 24, 65
6.49 + \item {\tt <} constant, 75
6.50 + \item {\tt <} symbol, 76
6.51 + \item {\tt <->} symbol, 6, 98
6.52 + \item {\tt <=} constant, 75
6.53 + \item {\tt <=} symbol, 24, 65
6.54 + \item {\tt =} symbol, 6, 58, 98, 112
6.55 + \item {\tt ?} symbol, 58, 60, 66, 68
6.56 + \item {\tt ?!} symbol, 58
6.57 + \item {\tt\at} symbol, 58, 79
6.58 + \item {\tt `} symbol, 24, 112
6.59 + \item {\tt ``} symbol, 24, 65
6.60 + \item \verb'{}' symbol, 65
6.61 + \item {\tt |} symbol, 6, 58, 98
6.62 + \item {\tt |-|} symbol, 121
6.63
6.64 \indexspace
6.65
6.66 - \item {\ptt 0} constant, 24, 78, 111
6.67 + \item {\tt 0} constant, 24, 76, 110
6.68
6.69 \indexspace
6.70
6.71 - \item {\ptt absdiff_def} theorem, 122
6.72 - \item {\ptt add_0} theorem, 79
6.73 - \item {\ptt add_assoc} theorem, 122
6.74 - \item {\ptt add_commute} theorem, 122
6.75 - \item {\ptt add_def} theorem, 46, 122
6.76 - \item {\ptt add_inverse_diff} theorem, 122
6.77 - \item {\ptt add_mp_tac}, \bold{121}
6.78 - \item {\ptt add_mult_dist} theorem, 46, 122
6.79 - \item {\ptt add_safes}, \bold{105}
6.80 - \item {\ptt add_Suc} theorem, 79
6.81 - \item {\ptt add_typing} theorem, 122
6.82 - \item {\ptt add_unsafes}, \bold{105}
6.83 - \item {\ptt addC0} theorem, 122
6.84 - \item {\ptt addC_succ} theorem, 122
6.85 - \item {\ptt ALL} symbol, 6, 25, 59, 61, 67, 69, 99
6.86 - \item {\ptt All} constant, 6, 59, 99
6.87 - \item {\ptt All_def} theorem, 62
6.88 - \item {\ptt all_dupE} theorem, 4, 8, 65
6.89 - \item {\ptt all_impE} theorem, 8
6.90 - \item {\ptt allE} theorem, 4, 8, 65
6.91 - \item {\ptt allI} theorem, 7, 65
6.92 - \item {\ptt allL} theorem, 101, 104
6.93 - \item {\ptt allL_thin} theorem, 102
6.94 - \item {\ptt allR} theorem, 101
6.95 - \item {\ptt and_def} theorem, 42, 62
6.96 - \item {\ptt app_def} theorem, 48
6.97 - \item {\ptt append_Cons} theorem, 81
6.98 - \item {\ptt append_Nil} theorem, 81
6.99 - \item {\ptt apply_def} theorem, 30
6.100 - \item {\ptt apply_equality} theorem, 38, 40, 56
6.101 - \item {\ptt apply_equality2} theorem, 38
6.102 - \item {\ptt apply_iff} theorem, 38
6.103 - \item {\ptt apply_Pair} theorem, 38, 56
6.104 - \item {\ptt apply_type} theorem, 38
6.105 - \item {\ptt arg_cong} theorem, 64
6.106 - \item {\ptt Arith} theory, 43, 77, 121
6.107 + \item {\tt absdiff_def} theorem, 121
6.108 + \item {\tt add_assoc} theorem, 121
6.109 + \item {\tt add_commute} theorem, 121
6.110 + \item {\tt add_def} theorem, 46, 121
6.111 + \item {\tt add_inverse_diff} theorem, 121
6.112 + \item {\tt add_mp_tac}, \bold{119}
6.113 + \item {\tt add_mult_dist} theorem, 46, 121
6.114 + \item {\tt add_safes}, \bold{104}
6.115 + \item {\tt add_typing} theorem, 121
6.116 + \item {\tt add_unsafes}, \bold{104}
6.117 + \item {\tt addC0} theorem, 121
6.118 + \item {\tt addC_succ} theorem, 121
6.119 + \item {\tt ALL} symbol, 6, 25, 58, 60, 66, 68, 98
6.120 + \item {\tt All} constant, 6, 58, 98
6.121 + \item {\tt All_def} theorem, 62
6.122 + \item {\tt all_dupE} theorem, 4, 8, 64
6.123 + \item {\tt all_impE} theorem, 8
6.124 + \item {\tt allE} theorem, 4, 8, 64
6.125 + \item {\tt allI} theorem, 7, 64
6.126 + \item {\tt allL} theorem, 100, 103
6.127 + \item {\tt allL_thin} theorem, 101
6.128 + \item {\tt allR} theorem, 100
6.129 + \item {\tt and_def} theorem, 41, 62
6.130 + \item {\tt app_def} theorem, 48
6.131 + \item {\tt apply_def} theorem, 30
6.132 + \item {\tt apply_equality} theorem, 38, 39, 55
6.133 + \item {\tt apply_equality2} theorem, 38
6.134 + \item {\tt apply_iff} theorem, 38
6.135 + \item {\tt apply_Pair} theorem, 38, 55, 56
6.136 + \item {\tt apply_type} theorem, 38
6.137 + \item {\tt arg_cong} theorem, 63
6.138 + \item {\tt Arith} theory, 45, 77, 120
6.139 \item assumptions
6.140 \subitem contradictory, 15
6.141 - \subitem in {\CTT}, 110, 120
6.142 + \subitem in {\CTT}, 109, 119
6.143
6.144 \indexspace
6.145
6.146 - \item {\ptt Ball} constant, 24, 28, 66, 69
6.147 - \item {\ptt ball_cong} theorem, 31, 32
6.148 - \item {\ptt Ball_def} theorem, 29, 69
6.149 - \item {\ptt ballE} theorem, 31, 32, 70
6.150 - \item {\ptt ballI} theorem, 32, 70
6.151 - \item {\ptt basic} theorem, 101
6.152 - \item {\ptt basic_defs}, \bold{119}
6.153 - \item {\ptt best_tac}, \bold{106}
6.154 - \item {\ptt beta} theorem, 39, 40
6.155 - \item {\ptt Bex} constant, 24, 28, 66, 69
6.156 - \item {\ptt bex_cong} theorem, 31, 32
6.157 - \item {\ptt Bex_def} theorem, 29, 69
6.158 - \item {\ptt bexCI} theorem, 32, 70, 72
6.159 - \item {\ptt bexE} theorem, 32, 70
6.160 - \item {\ptt bexI} theorem, 32, 70, 72
6.161 - \item {\ptt bij} constant, 45
6.162 - \item {\ptt bij_converse_bij} theorem, 45
6.163 - \item {\ptt bij_def} theorem, 45
6.164 - \item {\ptt bij_disjoint_Un} theorem, 45
6.165 - \item {\ptt bnd_mono_def} theorem, 44
6.166 - \item {\ptt Bool} theory, 40
6.167 - \item {\ptt bool} type, 60
6.168 - \item {\ptt bool_0I} theorem, 42
6.169 - \item {\ptt bool_1I} theorem, 42
6.170 - \item {\ptt bool_def} theorem, 42
6.171 - \item {\ptt boolE} theorem, 42
6.172 - \item {\ptt box_equals} theorem, 63, 64
6.173 - \item {\ptt bspec} theorem, 32, 70
6.174 + \item {\tt Ball} constant, 24, 28, 65, 68
6.175 + \item {\tt ball_cong} theorem, 31, 32
6.176 + \item {\tt Ball_def} theorem, 29, 68
6.177 + \item {\tt ballE} theorem, 31, 32, 69
6.178 + \item {\tt ballI} theorem, 32, 69
6.179 + \item {\tt basic} theorem, 100
6.180 + \item {\tt basic_defs}, \bold{117}
6.181 + \item {\tt best_tac}, \bold{105}
6.182 + \item {\tt beta} theorem, 38, 39
6.183 + \item {\tt Bex} constant, 24, 28, 65, 68
6.184 + \item {\tt bex_cong} theorem, 31, 32
6.185 + \item {\tt Bex_def} theorem, 29, 68
6.186 + \item {\tt bexCI} theorem, 32, 69, 72
6.187 + \item {\tt bexE} theorem, 32, 69
6.188 + \item {\tt bexI} theorem, 32, 69, 72
6.189 + \item {\tt bij} constant, 44
6.190 + \item {\tt bij_converse_bij} theorem, 44
6.191 + \item {\tt bij_def} theorem, 44
6.192 + \item {\tt bij_disjoint_Un} theorem, 44
6.193 + \item {\tt bnd_mono_def} theorem, 43
6.194 + \item {\tt Bool} theory, 39
6.195 + \item {\tt bool} type, 59
6.196 + \item {\tt bool_0I} theorem, 41
6.197 + \item {\tt bool_1I} theorem, 41
6.198 + \item {\tt bool_def} theorem, 41
6.199 + \item {\tt boolE} theorem, 41
6.200 + \item {\tt box_equals} theorem, 62, 63
6.201 + \item {\tt bspec} theorem, 32, 69
6.202
6.203 \indexspace
6.204
6.205 - \item {\ptt case} constant, 42
6.206 - \item {\ptt case} symbol, 61, 82, 86
6.207 - \item {\ptt case_def} theorem, 42
6.208 - \item {\ptt case_Inl} theorem, 42
6.209 - \item {\ptt case_Inr} theorem, 42
6.210 - \item {\ptt case_tac}, \bold{63}
6.211 - \item {\ptt CCL} theory, 1
6.212 - \item {\ptt ccontr} theorem, 65
6.213 - \item {\ptt classical} theorem, 65
6.214 - \item {\ptt coinduct} theorem, 44
6.215 - \item {\ptt coinductive}, 91--94
6.216 - \item {\ptt Collect} constant, 24, 25, 28, 66, 68
6.217 - \item {\ptt Collect_def} theorem, 29
6.218 - \item {\ptt Collect_mem_eq} theorem, 69
6.219 - \item {\ptt Collect_subset} theorem, 35
6.220 - \item {\ptt CollectD} theorem, 70, 96
6.221 - \item {\ptt CollectD1} theorem, 31, 33
6.222 - \item {\ptt CollectD2} theorem, 31, 33
6.223 - \item {\ptt CollectE} theorem, 31, 33, 70
6.224 - \item {\ptt CollectI} theorem, 33, 70, 97
6.225 - \item {\ptt comp_assoc} theorem, 45
6.226 - \item {\ptt comp_bij} theorem, 45
6.227 - \item {\ptt comp_def} theorem, 45
6.228 - \item {\ptt comp_func} theorem, 45
6.229 - \item {\ptt comp_func_apply} theorem, 45
6.230 - \item {\ptt comp_inj} theorem, 45
6.231 - \item {\ptt comp_rls}, \bold{119}
6.232 - \item {\ptt comp_surj} theorem, 45
6.233 - \item {\ptt comp_type} theorem, 45
6.234 - \item {\ptt Compl} constant, 66
6.235 - \item {\ptt Compl_def} theorem, 69
6.236 - \item {\ptt Compl_disjoint} theorem, 73
6.237 - \item {\ptt Compl_Int} theorem, 73
6.238 - \item {\ptt Compl_partition} theorem, 73
6.239 - \item {\ptt Compl_Un} theorem, 73
6.240 - \item {\ptt ComplD} theorem, 71
6.241 - \item {\ptt ComplI} theorem, 71
6.242 - \item {\ptt cond_0} theorem, 42
6.243 - \item {\ptt cond_1} theorem, 42
6.244 - \item {\ptt cond_def} theorem, 42
6.245 - \item {\ptt cong} theorem, 64
6.246 + \item {\tt case} constant, 42
6.247 + \item {\tt case} symbol, 61, 77, 78, 84
6.248 + \item {\tt case_def} theorem, 42
6.249 + \item {\tt case_Inl} theorem, 42
6.250 + \item {\tt case_Inr} theorem, 42
6.251 + \item {\tt case_tac}, \bold{62}
6.252 + \item {\tt CCL} theory, 1
6.253 + \item {\tt ccontr} theorem, 64
6.254 + \item {\tt classical} theorem, 64
6.255 + \item {\tt coinduct} theorem, 43
6.256 + \item {\tt coinductive}, 90--93
6.257 + \item {\tt Collect} constant, 24, 25, 28, 65, 67
6.258 + \item {\tt Collect_def} theorem, 29
6.259 + \item {\tt Collect_mem_eq} theorem, 68
6.260 + \item {\tt Collect_subset} theorem, 35
6.261 + \item {\tt CollectD} theorem, 69, 95
6.262 + \item {\tt CollectD1} theorem, 31, 33
6.263 + \item {\tt CollectD2} theorem, 31, 33
6.264 + \item {\tt CollectE} theorem, 31, 33, 69
6.265 + \item {\tt CollectI} theorem, 33, 69, 96
6.266 + \item {\tt comp_assoc} theorem, 44
6.267 + \item {\tt comp_bij} theorem, 44
6.268 + \item {\tt comp_def} theorem, 44
6.269 + \item {\tt comp_func} theorem, 44
6.270 + \item {\tt comp_func_apply} theorem, 44
6.271 + \item {\tt comp_inj} theorem, 44
6.272 + \item {\tt comp_rls}, \bold{117}
6.273 + \item {\tt comp_surj} theorem, 44
6.274 + \item {\tt comp_type} theorem, 44
6.275 + \item {\tt Compl} constant, 65
6.276 + \item {\tt Compl_def} theorem, 68
6.277 + \item {\tt Compl_disjoint} theorem, 71
6.278 + \item {\tt Compl_Int} theorem, 71
6.279 + \item {\tt Compl_partition} theorem, 71
6.280 + \item {\tt Compl_Un} theorem, 71
6.281 + \item {\tt ComplD} theorem, 70
6.282 + \item {\tt ComplI} theorem, 70
6.283 + \item {\tt concat} constant, 79
6.284 + \item {\tt cond_0} theorem, 41
6.285 + \item {\tt cond_1} theorem, 41
6.286 + \item {\tt cond_def} theorem, 41
6.287 + \item {\tt cong} theorem, 63
6.288 \item congruence rules, 31
6.289 - \item {\ptt conj_cong}, 74
6.290 - \item {\ptt conj_impE} theorem, 5, 8
6.291 - \item {\ptt conjE} theorem, 8, 64
6.292 - \item {\ptt conjI} theorem, 7, 64
6.293 - \item {\ptt conjL} theorem, 101
6.294 - \item {\ptt conjR} theorem, 101
6.295 - \item {\ptt conjunct1} theorem, 7, 64
6.296 - \item {\ptt conjunct2} theorem, 7, 64
6.297 - \item {\ptt conL} theorem, 102
6.298 - \item {\ptt conR} theorem, 102
6.299 - \item {\ptt cons} constant, 24, 25
6.300 - \item {\ptt cons_def} theorem, 30
6.301 - \item {\ptt Cons_iff} theorem, 48
6.302 - \item {\ptt consCI} theorem, 34
6.303 - \item {\ptt consE} theorem, 34
6.304 - \item {\ptt ConsI} theorem, 48
6.305 - \item {\ptt consI1} theorem, 34
6.306 - \item {\ptt consI2} theorem, 34
6.307 - \item Constructive Type Theory, 110--133
6.308 - \item {\ptt contr} constant, 111
6.309 - \item {\ptt converse} constant, 24, 37
6.310 - \item {\ptt converse_def} theorem, 30
6.311 - \item {\ptt could_res}, \bold{103}
6.312 - \item {\ptt could_resolve_seq}, \bold{104}
6.313 - \item {\ptt CTT} theory, 1, 110
6.314 - \item {\ptt Cube} theory, 1
6.315 - \item {\ptt cut} theorem, 101
6.316 - \item {\ptt cut_facts_tac}, 17, 18, 55
6.317 - \item {\ptt cutL_tac}, \bold{103}
6.318 - \item {\ptt cutR_tac}, \bold{103}
6.319 + \item {\tt conj_cong}, 73
6.320 + \item {\tt conj_impE} theorem, 5, 8
6.321 + \item {\tt conjE} theorem, 8, 63
6.322 + \item {\tt conjI} theorem, 7, 63
6.323 + \item {\tt conjL} theorem, 100
6.324 + \item {\tt conjR} theorem, 100
6.325 + \item {\tt conjunct1} theorem, 7, 63
6.326 + \item {\tt conjunct2} theorem, 7, 63
6.327 + \item {\tt conL} theorem, 101
6.328 + \item {\tt conR} theorem, 101
6.329 + \item {\tt cons} constant, 24, 25
6.330 + \item {\tt cons_def} theorem, 30
6.331 + \item {\tt Cons_iff} theorem, 48
6.332 + \item {\tt consCI} theorem, 34
6.333 + \item {\tt consE} theorem, 34
6.334 + \item {\tt ConsI} theorem, 48
6.335 + \item {\tt consI1} theorem, 34
6.336 + \item {\tt consI2} theorem, 34
6.337 + \item Constructive Type Theory, 109--131
6.338 + \item {\tt contr} constant, 110
6.339 + \item {\tt converse} constant, 24, 38
6.340 + \item {\tt converse_def} theorem, 30
6.341 + \item {\tt could_res}, \bold{102}
6.342 + \item {\tt could_resolve_seq}, \bold{103}
6.343 + \item {\tt CTT} theory, 1, 109
6.344 + \item {\tt Cube} theory, 1
6.345 + \item {\tt cut} theorem, 100
6.346 + \item {\tt cut_facts_tac}, 17, 18, 54
6.347 + \item {\tt cutL_tac}, \bold{102}
6.348 + \item {\tt cutR_tac}, \bold{102}
6.349
6.350 \indexspace
6.351
6.352 - \item {\ptt datatype}, 85--91
6.353 - \item {\ptt deepen_tac}, 15
6.354 - \item {\ptt diff_0} theorem, 79
6.355 - \item {\ptt diff_0_eq_0} theorem, 79, 122
6.356 - \item {\ptt Diff_cancel} theorem, 41
6.357 - \item {\ptt Diff_contains} theorem, 35
6.358 - \item {\ptt Diff_def} theorem, 29
6.359 - \item {\ptt diff_def} theorem, 46, 122
6.360 - \item {\ptt Diff_disjoint} theorem, 41
6.361 - \item {\ptt Diff_Int} theorem, 41
6.362 - \item {\ptt Diff_partition} theorem, 41
6.363 - \item {\ptt diff_self_eq_0} theorem, 122
6.364 - \item {\ptt Diff_subset} theorem, 35
6.365 - \item {\ptt diff_Suc_Suc} theorem, 79
6.366 - \item {\ptt diff_succ_succ} theorem, 122
6.367 - \item {\ptt diff_typing} theorem, 122
6.368 - \item {\ptt Diff_Un} theorem, 41
6.369 - \item {\ptt diffC0} theorem, 122
6.370 - \item {\ptt DiffD1} theorem, 34
6.371 - \item {\ptt DiffD2} theorem, 34
6.372 - \item {\ptt DiffE} theorem, 34
6.373 - \item {\ptt DiffI} theorem, 34
6.374 - \item {\ptt disj_impE} theorem, 5, 8, 13
6.375 - \item {\ptt disjCI} theorem, 10, 65
6.376 - \item {\ptt disjE} theorem, 7, 64
6.377 - \item {\ptt disjI1} theorem, 7, 64
6.378 - \item {\ptt disjI2} theorem, 7, 64
6.379 - \item {\ptt disjL} theorem, 101
6.380 - \item {\ptt disjR} theorem, 101
6.381 - \item {\ptt div} symbol, 46, 78, 122
6.382 - \item {\ptt div_def} theorem, 46, 122
6.383 - \item {\ptt div_geq} theorem, 79
6.384 - \item {\ptt div_less} theorem, 79
6.385 - \item {\ptt domain} constant, 24, 38
6.386 - \item {\ptt domain_def} theorem, 30
6.387 - \item {\ptt domain_of_fun} theorem, 38
6.388 - \item {\ptt domain_subset} theorem, 37
6.389 - \item {\ptt domain_type} theorem, 38
6.390 - \item {\ptt domainE} theorem, 37, 38
6.391 - \item {\ptt domainI} theorem, 37, 38
6.392 - \item {\ptt double_complement} theorem, 41, 73
6.393 - \item {\ptt dresolve_tac}, 53
6.394 + \item {\tt datatype}, 83--90
6.395 + \item {\tt deepen_tac}, 15
6.396 + \item {\tt diff_0_eq_0} theorem, 121
6.397 + \item {\tt Diff_cancel} theorem, 40
6.398 + \item {\tt Diff_contains} theorem, 35
6.399 + \item {\tt Diff_def} theorem, 29
6.400 + \item {\tt diff_def} theorem, 46, 121
6.401 + \item {\tt Diff_disjoint} theorem, 40
6.402 + \item {\tt Diff_Int} theorem, 40
6.403 + \item {\tt Diff_partition} theorem, 40
6.404 + \item {\tt diff_self_eq_0} theorem, 121
6.405 + \item {\tt Diff_subset} theorem, 35
6.406 + \item {\tt diff_succ_succ} theorem, 121
6.407 + \item {\tt diff_typing} theorem, 121
6.408 + \item {\tt Diff_Un} theorem, 40
6.409 + \item {\tt diffC0} theorem, 121
6.410 + \item {\tt DiffD1} theorem, 34
6.411 + \item {\tt DiffD2} theorem, 34
6.412 + \item {\tt DiffE} theorem, 34
6.413 + \item {\tt DiffI} theorem, 34
6.414 + \item {\tt disj_impE} theorem, 5, 8, 13
6.415 + \item {\tt disjCI} theorem, 10, 64
6.416 + \item {\tt disjE} theorem, 7, 63
6.417 + \item {\tt disjI1} theorem, 7, 63
6.418 + \item {\tt disjI2} theorem, 7, 63
6.419 + \item {\tt disjL} theorem, 100
6.420 + \item {\tt disjR} theorem, 100
6.421 + \item {\tt div} symbol, 46, 76, 121
6.422 + \item {\tt div_def} theorem, 46, 121
6.423 + \item {\tt div_geq} theorem, 77
6.424 + \item {\tt div_less} theorem, 77
6.425 + \item {\tt domain} constant, 24, 38
6.426 + \item {\tt domain_def} theorem, 30
6.427 + \item {\tt domain_of_fun} theorem, 38
6.428 + \item {\tt domain_subset} theorem, 37
6.429 + \item {\tt domain_type} theorem, 38
6.430 + \item {\tt domainE} theorem, 37, 38
6.431 + \item {\tt domainI} theorem, 37, 38
6.432 + \item {\tt double_complement} theorem, 40, 71
6.433 + \item {\tt dresolve_tac}, 52
6.434 + \item {\tt drop} constant, 79
6.435 + \item {\tt dropWhile} constant, 79
6.436
6.437 \indexspace
6.438
6.439 - \item {\ptt Elem} constant, 111
6.440 - \item {\ptt elim_rls}, \bold{119}
6.441 - \item {\ptt elimL_rls}, \bold{119}
6.442 - \item {\ptt empty_def} theorem, 69
6.443 - \item {\ptt empty_pack}, \bold{104}
6.444 - \item {\ptt empty_subsetI} theorem, 32
6.445 - \item {\ptt emptyE} theorem, 32, 71
6.446 - \item {\ptt Eps} constant, 59, 61
6.447 - \item {\ptt Eq} constant, 111
6.448 - \item {\ptt eq} constant, 111, 118
6.449 - \item {\ptt eq_mp_tac}, \bold{9}
6.450 - \item {\ptt EqC} theorem, 118
6.451 - \item {\ptt EqE} theorem, 118
6.452 - \item {\ptt Eqelem} constant, 111
6.453 - \item {\ptt EqF} theorem, 118
6.454 - \item {\ptt EqFL} theorem, 118
6.455 - \item {\ptt EqI} theorem, 118
6.456 - \item {\ptt Eqtype} constant, 111
6.457 - \item {\ptt equal_tac}, \bold{120}
6.458 - \item {\ptt equal_types} theorem, 114
6.459 - \item {\ptt equal_typesL} theorem, 114
6.460 - \item {\ptt equalityCE} theorem, 70, 72, 96, 97
6.461 - \item {\ptt equalityD1} theorem, 32, 70
6.462 - \item {\ptt equalityD2} theorem, 32, 70
6.463 - \item {\ptt equalityE} theorem, 32, 70
6.464 - \item {\ptt equalityI} theorem, 32, 52, 54, 70
6.465 - \item {\ptt equals0D} theorem, 32
6.466 - \item {\ptt equals0I} theorem, 32
6.467 - \item {\ptt eresolve_tac}, 15
6.468 - \item {\ptt eta} theorem, 39, 40
6.469 - \item {\ptt EX} symbol, 6, 25, 59, 61, 67, 69, 99
6.470 - \item {\ptt Ex} constant, 6, 59, 99
6.471 - \item {\ptt EX!} symbol, 6, 59
6.472 - \item {\ptt Ex1} constant, 6, 59
6.473 - \item {\ptt Ex1_def} theorem, 62
6.474 - \item {\ptt ex1_def} theorem, 7
6.475 - \item {\ptt ex1E} theorem, 8, 65
6.476 - \item {\ptt ex1I} theorem, 8, 65
6.477 - \item {\ptt Ex_def} theorem, 62
6.478 - \item {\ptt ex_impE} theorem, 8
6.479 - \item {\ptt exCI} theorem, 10, 14, 65
6.480 - \item {\ptt excluded_middle} theorem, 10, 65
6.481 - \item {\ptt exE} theorem, 7, 65
6.482 - \item {\ptt exI} theorem, 7, 65
6.483 - \item {\ptt exL} theorem, 101
6.484 - \item {\ptt expand_if} theorem, 65
6.485 - \item {\ptt expand_split} theorem, 75
6.486 - \item {\ptt expand_sum_case} theorem, 77
6.487 - \item {\ptt exR} theorem, 101, 104, 106
6.488 - \item {\ptt exR_thin} theorem, 102, 106, 107
6.489 - \item {\ptt ext} theorem, 62, 63
6.490 - \item {\ptt extension} theorem, 29
6.491 + \item {\tt Elem} constant, 110
6.492 + \item {\tt elim_rls}, \bold{117}
6.493 + \item {\tt elimL_rls}, \bold{117}
6.494 + \item {\tt empty_def} theorem, 68
6.495 + \item {\tt empty_pack}, \bold{103}
6.496 + \item {\tt empty_subsetI} theorem, 32
6.497 + \item {\tt emptyE} theorem, 32, 70
6.498 + \item {\tt Eps} constant, 58, 60
6.499 + \item {\tt Eq} constant, 110
6.500 + \item {\tt eq} constant, 110, 115
6.501 + \item {\tt eq_mp_tac}, \bold{9}
6.502 + \item {\tt EqC} theorem, 116
6.503 + \item {\tt EqE} theorem, 116
6.504 + \item {\tt Eqelem} constant, 110
6.505 + \item {\tt EqF} theorem, 116
6.506 + \item {\tt EqFL} theorem, 116
6.507 + \item {\tt EqI} theorem, 116
6.508 + \item {\tt Eqtype} constant, 110
6.509 + \item {\tt equal_tac}, \bold{118}
6.510 + \item {\tt equal_types} theorem, 113
6.511 + \item {\tt equal_typesL} theorem, 113
6.512 + \item {\tt equalityCE} theorem, 69, 72, 95, 96
6.513 + \item {\tt equalityD1} theorem, 32, 69
6.514 + \item {\tt equalityD2} theorem, 32, 69
6.515 + \item {\tt equalityE} theorem, 32, 69
6.516 + \item {\tt equalityI} theorem, 32, 51, 53, 69
6.517 + \item {\tt equals0D} theorem, 32
6.518 + \item {\tt equals0I} theorem, 32
6.519 + \item {\tt eresolve_tac}, 15
6.520 + \item {\tt eta} theorem, 38, 39
6.521 + \item {\tt EX} symbol, 6, 25, 58, 60, 66, 68, 98
6.522 + \item {\tt Ex} constant, 6, 58, 98
6.523 + \item {\tt EX!} symbol, 6, 58
6.524 + \item {\tt Ex1} constant, 6, 58
6.525 + \item {\tt Ex1_def} theorem, 62
6.526 + \item {\tt ex1_def} theorem, 7
6.527 + \item {\tt ex1E} theorem, 8, 64
6.528 + \item {\tt ex1I} theorem, 8, 64
6.529 + \item {\tt Ex_def} theorem, 62
6.530 + \item {\tt ex_impE} theorem, 8
6.531 + \item {\tt exCI} theorem, 10, 14, 64
6.532 + \item {\tt excluded_middle} theorem, 10, 64
6.533 + \item {\tt exE} theorem, 7, 64
6.534 + \item {\tt exI} theorem, 7, 64
6.535 + \item {\tt exL} theorem, 100
6.536 + \item {\tt expand_if} theorem, 64
6.537 + \item {\tt expand_split} theorem, 74
6.538 + \item {\tt expand_sum_case} theorem, 76
6.539 + \item {\tt exR} theorem, 100, 103, 105
6.540 + \item {\tt exR_thin} theorem, 101, 105, 106
6.541 + \item {\tt ext} theorem, 61
6.542 + \item {\tt extension} theorem, 29
6.543
6.544 \indexspace
6.545
6.546 - \item {\ptt F} constant, 111
6.547 - \item {\ptt f_Inv_f} theorem, 72
6.548 - \item {\ptt False} constant, 6, 59, 99
6.549 - \item {\ptt False_def} theorem, 62
6.550 - \item {\ptt FalseE} theorem, 7, 64
6.551 - \item {\ptt FalseL} theorem, 101
6.552 - \item {\ptt Fast_tac}, 53
6.553 - \item {\ptt fast_tac}, 17, 19, 20, 55, \bold{106}
6.554 - \item {\ptt FE} theorem, 117, 121
6.555 - \item {\ptt FEL} theorem, 117
6.556 - \item {\ptt FF} theorem, 117
6.557 - \item {\ptt field} constant, 24
6.558 - \item {\ptt field_def} theorem, 30
6.559 - \item {\ptt field_subset} theorem, 37
6.560 - \item {\ptt fieldCI} theorem, 37
6.561 - \item {\ptt fieldE} theorem, 37
6.562 - \item {\ptt fieldI1} theorem, 37
6.563 - \item {\ptt fieldI2} theorem, 37
6.564 - \item {\ptt filseq_resolve_tac}, \bold{104}
6.565 - \item {\ptt filt_resolve_tac}, 104, 119
6.566 - \item {\ptt filter} constant, 80
6.567 - \item {\ptt filter_Cons} theorem, 81
6.568 - \item {\ptt filter_Nil} theorem, 81
6.569 - \item {\ptt Fin.consI} theorem, 47
6.570 - \item {\ptt Fin.emptyI} theorem, 47
6.571 - \item {\ptt Fin_induct} theorem, 47
6.572 - \item {\ptt Fin_mono} theorem, 47
6.573 - \item {\ptt Fin_subset} theorem, 47
6.574 - \item {\ptt Fin_UnI} theorem, 47
6.575 - \item {\ptt Fin_UnionI} theorem, 47
6.576 + \item {\tt F} constant, 110
6.577 + \item {\tt False} constant, 6, 58, 98
6.578 + \item {\tt False_def} theorem, 62
6.579 + \item {\tt FalseE} theorem, 7, 63
6.580 + \item {\tt FalseL} theorem, 100
6.581 + \item {\tt Fast_tac}, 53
6.582 + \item {\tt fast_tac}, 17, 19, 20, 54, \bold{105}
6.583 + \item {\tt FE} theorem, 116, 120
6.584 + \item {\tt FEL} theorem, 116
6.585 + \item {\tt FF} theorem, 116
6.586 + \item {\tt field} constant, 24
6.587 + \item {\tt field_def} theorem, 30
6.588 + \item {\tt field_subset} theorem, 37
6.589 + \item {\tt fieldCI} theorem, 37
6.590 + \item {\tt fieldE} theorem, 37
6.591 + \item {\tt fieldI1} theorem, 37
6.592 + \item {\tt fieldI2} theorem, 37
6.593 + \item {\tt filseq_resolve_tac}, \bold{103}
6.594 + \item {\tt filt_resolve_tac}, 103, 118
6.595 + \item {\tt filter} constant, 79
6.596 + \item {\tt Fin.consI} theorem, 47
6.597 + \item {\tt Fin.emptyI} theorem, 47
6.598 + \item {\tt Fin_induct} theorem, 47
6.599 + \item {\tt Fin_mono} theorem, 47
6.600 + \item {\tt Fin_subset} theorem, 47
6.601 + \item {\tt Fin_UnI} theorem, 47
6.602 + \item {\tt Fin_UnionI} theorem, 47
6.603 \item first-order logic, 4--21
6.604 - \item {\ptt Fixedpt} theory, 40
6.605 - \item {\ptt flat} constant, 48, 80
6.606 - \item {\ptt flat_Cons} theorem, 81
6.607 - \item {\ptt flat_def} theorem, 48
6.608 - \item {\ptt flat_Nil} theorem, 81
6.609 - \item flex-flex constraints, 98
6.610 - \item {\ptt FOL} theory, 1, 4, 10, 121
6.611 - \item {\ptt FOL_cs}, \bold{10}
6.612 - \item {\ptt FOL_ss}, \bold{5}
6.613 - \item {\ptt foldl} constant, 80
6.614 - \item {\ptt foldl_Cons} theorem, 81
6.615 - \item {\ptt foldl_Nil} theorem, 81
6.616 - \item {\ptt form_rls}, \bold{119}
6.617 - \item {\ptt formL_rls}, \bold{119}
6.618 - \item {\ptt forms_of_seq}, \bold{103}
6.619 - \item {\ptt foundation} theorem, 29
6.620 - \item {\ptt fst} constant, 24, 31, 75, 111, 118
6.621 - \item {\ptt fst_conv} theorem, 36, 75
6.622 - \item {\ptt fst_def} theorem, 30, 116
6.623 - \item {\ptt fun} type, 60
6.624 - \item {\ptt fun_cong} theorem, 64
6.625 - \item {\ptt fun_disjoint_apply1} theorem, 39, 55
6.626 - \item {\ptt fun_disjoint_apply2} theorem, 39
6.627 - \item {\ptt fun_disjoint_Un} theorem, 39, 57
6.628 - \item {\ptt fun_empty} theorem, 39
6.629 - \item {\ptt fun_extension} theorem, 38, 40
6.630 - \item {\ptt fun_is_rel} theorem, 38
6.631 - \item {\ptt fun_single} theorem, 39
6.632 + \item {\tt Fixedpt} theory, 41
6.633 + \item {\tt flat} constant, 48
6.634 + \item {\tt flat_def} theorem, 48
6.635 + \item flex-flex constraints, 97
6.636 + \item {\tt FOL} theory, 1, 4, 10, 119
6.637 + \item {\tt FOL_cs}, \bold{10}
6.638 + \item {\tt FOL_ss}, \bold{5}
6.639 + \item {\tt foldl} constant, 79
6.640 + \item {\tt form_rls}, \bold{117}
6.641 + \item {\tt formL_rls}, \bold{117}
6.642 + \item {\tt forms_of_seq}, \bold{102}
6.643 + \item {\tt foundation} theorem, 29
6.644 + \item {\tt fst} constant, 24, 28, 74, 110, 115
6.645 + \item {\tt fst_conv} theorem, 36, 74
6.646 + \item {\tt fst_def} theorem, 30, 115
6.647 + \item {\tt Fun} theory, 72
6.648 + \item {\tt fun} type, 59
6.649 + \item {\tt fun_cong} theorem, 63
6.650 + \item {\tt fun_disjoint_apply1} theorem, 39, 55
6.651 + \item {\tt fun_disjoint_apply2} theorem, 39
6.652 + \item {\tt fun_disjoint_Un} theorem, 39, 56
6.653 + \item {\tt fun_empty} theorem, 39
6.654 + \item {\tt fun_extension} theorem, 38, 39
6.655 + \item {\tt fun_is_rel} theorem, 38
6.656 + \item {\tt fun_single} theorem, 39
6.657 \item function applications
6.658 - \subitem in \CTT, 113
6.659 + \subitem in \CTT, 112
6.660 \subitem in \ZF, 24
6.661
6.662 \indexspace
6.663
6.664 - \item {\ptt gfp_def} theorem, 44
6.665 - \item {\ptt gfp_least} theorem, 44
6.666 - \item {\ptt gfp_mono} theorem, 44
6.667 - \item {\ptt gfp_subset} theorem, 44
6.668 - \item {\ptt gfp_Tarski} theorem, 44
6.669 - \item {\ptt gfp_upperbound} theorem, 44
6.670 - \item {\ptt goalw}, 17
6.671 + \item {\tt gfp_def} theorem, 43
6.672 + \item {\tt gfp_least} theorem, 43
6.673 + \item {\tt gfp_mono} theorem, 43
6.674 + \item {\tt gfp_subset} theorem, 43
6.675 + \item {\tt gfp_Tarski} theorem, 43
6.676 + \item {\tt gfp_upperbound} theorem, 43
6.677 + \item {\tt goalw}, 17
6.678
6.679 \indexspace
6.680
6.681 - \item {\ptt hd} constant, 80
6.682 - \item {\ptt hd_Cons} theorem, 81
6.683 - \item higher-order logic, 58--97
6.684 - \item {\ptt HOL} theory, 1, 58
6.685 - \item {\sc hol} system, 58, 61
6.686 - \item {\ptt HOL_cs}, \bold{75}
6.687 - \item {\ptt HOL_quantifiers}, \bold{61}, 69
6.688 - \item {\ptt HOL_ss}, \bold{74}
6.689 - \item {\ptt HOLCF} theory, 1
6.690 - \item {\ptt hyp_rew_tac}, \bold{120}
6.691 - \item {\ptt hyp_subst_tac}, 5
6.692 + \item {\tt hd} constant, 79
6.693 + \item higher-order logic, 57--96
6.694 + \item {\tt HOL} theory, 1, 57
6.695 + \item {\sc hol} system, 57, 60
6.696 + \item {\tt HOL_cs}, \bold{73}
6.697 + \item {\tt HOL_quantifiers}, \bold{60}, 68
6.698 + \item {\tt HOL_ss}, \bold{73}
6.699 + \item {\tt HOLCF} theory, 1
6.700 + \item {\tt hyp_rew_tac}, \bold{119}
6.701 + \item {\tt hyp_subst_tac}, 5
6.702
6.703 \indexspace
6.704
6.705 - \item {\ptt i} type, 23, 110
6.706 - \item {\ptt id} constant, 45
6.707 - \item {\ptt id_def} theorem, 45
6.708 - \item {\ptt If} constant, 59
6.709 - \item {\ptt if} constant, 24
6.710 - \item {\ptt if_def} theorem, 16, 29, 62
6.711 - \item {\ptt if_not_P} theorem, 34, 65
6.712 - \item {\ptt if_P} theorem, 34, 65
6.713 - \item {\ptt ifE} theorem, 18
6.714 - \item {\ptt iff} theorem, 62, 63
6.715 - \item {\ptt iff_def} theorem, 7, 101
6.716 - \item {\ptt iff_impE} theorem, 8
6.717 - \item {\ptt iffCE} theorem, 10, 65, 72
6.718 - \item {\ptt iffD1} theorem, 8, 64
6.719 - \item {\ptt iffD2} theorem, 8, 64
6.720 - \item {\ptt iffE} theorem, 8, 64
6.721 - \item {\ptt iffI} theorem, 8, 18, 64
6.722 - \item {\ptt iffL} theorem, 102, 108
6.723 - \item {\ptt iffR} theorem, 102
6.724 - \item {\ptt ifI} theorem, 18
6.725 - \item {\ptt IFOL} theory, 4
6.726 - \item {\ptt IFOL_ss}, \bold{5}
6.727 - \item {\ptt image_def} theorem, 30, 69
6.728 - \item {\ptt imageE} theorem, 38, 72
6.729 - \item {\ptt imageI} theorem, 38, 72
6.730 - \item {\ptt imp_impE} theorem, 8, 13
6.731 - \item {\ptt impCE} theorem, 10, 65
6.732 - \item {\ptt impE} theorem, 8, 9, 64
6.733 - \item {\ptt impI} theorem, 7, 62
6.734 - \item {\ptt impL} theorem, 101
6.735 - \item {\ptt impR} theorem, 101
6.736 - \item {\ptt in} symbol, 26, 60
6.737 - \item {\ptt ind} type, 77
6.738 - \item {\ptt induct} theorem, 44
6.739 - \item {\ptt inductive}, 91--94
6.740 - \item {\ptt Inf} constant, 24, 28
6.741 - \item {\ptt infinity} theorem, 30
6.742 - \item {\ptt inj} constant, 45, 66
6.743 - \item {\ptt inj_converse_inj} theorem, 45
6.744 - \item {\ptt inj_def} theorem, 45, 69
6.745 - \item {\ptt inj_Inl} theorem, 77
6.746 - \item {\ptt inj_Inr} theorem, 77
6.747 - \item {\ptt inj_inverseI} theorem, 72
6.748 - \item {\ptt inj_onto} constant, 66, 72
6.749 - \item {\ptt inj_onto_contraD} theorem, 72
6.750 - \item {\ptt inj_onto_def} theorem, 69
6.751 - \item {\ptt inj_onto_inverseI} theorem, 72
6.752 - \item {\ptt inj_ontoD} theorem, 72
6.753 - \item {\ptt inj_ontoI} theorem, 72
6.754 - \item {\ptt inj_Suc} theorem, 78
6.755 - \item {\ptt injD} theorem, 72
6.756 - \item {\ptt injI} theorem, 72
6.757 - \item {\ptt Inl} constant, 42, 77
6.758 - \item {\ptt inl} constant, 111, 118, 126
6.759 - \item {\ptt Inl_def} theorem, 42
6.760 - \item {\ptt Inl_inject} theorem, 42
6.761 - \item {\ptt Inl_neq_Inr} theorem, 42
6.762 - \item {\ptt Inl_not_Inr} theorem, 77
6.763 - \item {\ptt Inr} constant, 42, 77
6.764 - \item {\ptt inr} constant, 111, 118
6.765 - \item {\ptt Inr_def} theorem, 42
6.766 - \item {\ptt Inr_inject} theorem, 42
6.767 - \item {\ptt insert} constant, 66
6.768 - \item {\ptt insert_def} theorem, 69
6.769 - \item {\ptt insertE} theorem, 71
6.770 - \item {\ptt insertI1} theorem, 71
6.771 - \item {\ptt insertI2} theorem, 71
6.772 - \item {\ptt INT} symbol, 25, 27, 66, 67, 69
6.773 - \item {\ptt Int} symbol, 24, 66
6.774 - \item {\ptt Int.best_tac}, \bold{9}
6.775 - \item {\ptt Int.fast_tac}, \bold{9}, 12
6.776 - \item {\ptt Int.inst_step_tac}, \bold{9}
6.777 - \item {\ptt Int.safe_step_tac}, \bold{9}
6.778 - \item {\ptt Int.safe_tac}, \bold{9}
6.779 - \item {\ptt Int.step_tac}, \bold{9}
6.780 - \item {\ptt Int_absorb} theorem, 41, 73
6.781 - \item {\ptt Int_assoc} theorem, 41, 73
6.782 - \item {\ptt Int_commute} theorem, 41, 73
6.783 - \item {\ptt INT_D} theorem, 71
6.784 - \item {\ptt Int_def} theorem, 29, 69
6.785 - \item {\ptt INT_E} theorem, 33, 71
6.786 - \item {\ptt Int_greatest} theorem, 35, 52, 53, 73
6.787 - \item {\ptt INT_I} theorem, 33, 71
6.788 - \item {\ptt Int_Inter_image} theorem, 73
6.789 - \item {\ptt Int_lower1} theorem, 35, 52, 73
6.790 - \item {\ptt Int_lower2} theorem, 35, 52, 73
6.791 - \item {\ptt Int_Un_distrib} theorem, 41, 73
6.792 - \item {\ptt Int_Union} theorem, 73
6.793 - \item {\ptt Int_Union_RepFun} theorem, 41
6.794 - \item {\ptt IntD1} theorem, 34, 71
6.795 - \item {\ptt IntD2} theorem, 34, 71
6.796 - \item {\ptt IntE} theorem, 34, 52, 71
6.797 - \item {\ptt INTER} constant, 66
6.798 - \item {\ptt Inter} constant, 24, 66
6.799 - \item {\ptt INTER1} constant, 66
6.800 - \item {\ptt INTER1_def} theorem, 69
6.801 - \item {\ptt INTER_def} theorem, 69
6.802 - \item {\ptt Inter_def} theorem, 29, 69
6.803 - \item {\ptt Inter_greatest} theorem, 35, 73
6.804 - \item {\ptt Inter_lower} theorem, 35, 73
6.805 - \item {\ptt Inter_Un_distrib} theorem, 41, 73
6.806 - \item {\ptt InterD} theorem, 33, 71
6.807 - \item {\ptt InterE} theorem, 33, 71
6.808 - \item {\ptt InterI} theorem, 31, 33, 71
6.809 - \item {\ptt IntI} theorem, 34, 71
6.810 - \item {\ptt intr_rls}, \bold{119}
6.811 - \item {\ptt intr_tac}, \bold{120}, 128--130
6.812 - \item {\ptt intrL_rls}, \bold{119}
6.813 - \item {\ptt Inv} constant, 59, 72
6.814 - \item {\ptt Inv_def} theorem, 62
6.815 - \item {\ptt Inv_f_f} theorem, 72
6.816 + \item {\tt i} type, 23, 109
6.817 + \item {\tt id} constant, 44
6.818 + \item {\tt id_def} theorem, 44
6.819 + \item {\tt If} constant, 58
6.820 + \item {\tt if} constant, 24
6.821 + \item {\tt if_def} theorem, 16, 29, 62
6.822 + \item {\tt if_not_P} theorem, 34, 64
6.823 + \item {\tt if_P} theorem, 34, 64
6.824 + \item {\tt ifE} theorem, 18
6.825 + \item {\tt iff} theorem, 61
6.826 + \item {\tt iff_def} theorem, 7, 100
6.827 + \item {\tt iff_impE} theorem, 8
6.828 + \item {\tt iffCE} theorem, 10, 64, 72
6.829 + \item {\tt iffD1} theorem, 8, 63
6.830 + \item {\tt iffD2} theorem, 8, 63
6.831 + \item {\tt iffE} theorem, 8, 63
6.832 + \item {\tt iffI} theorem, 8, 18, 63
6.833 + \item {\tt iffL} theorem, 101, 107
6.834 + \item {\tt iffR} theorem, 101
6.835 + \item {\tt ifI} theorem, 18
6.836 + \item {\tt IFOL} theory, 4
6.837 + \item {\tt IFOL_ss}, \bold{5}
6.838 + \item {\tt image_def} theorem, 30, 68
6.839 + \item {\tt imageE} theorem, 37, 70
6.840 + \item {\tt imageI} theorem, 37, 70
6.841 + \item {\tt imp_impE} theorem, 8, 13
6.842 + \item {\tt impCE} theorem, 10, 64
6.843 + \item {\tt impE} theorem, 8, 9, 63
6.844 + \item {\tt impI} theorem, 7, 61
6.845 + \item {\tt impL} theorem, 100
6.846 + \item {\tt impR} theorem, 100
6.847 + \item {\tt in} symbol, 26, 59
6.848 + \item {\tt ind} type, 75
6.849 + \item {\tt induct} theorem, 43
6.850 + \item {\tt induct_tac}, 77, 78, \bold{86}
6.851 + \item {\tt inductive}, 90--93
6.852 + \item {\tt Inf} constant, 24, 28
6.853 + \item {\tt infinity} theorem, 30
6.854 + \item {\tt inj} constant, 44, 72
6.855 + \item {\tt inj_converse_inj} theorem, 44
6.856 + \item {\tt inj_def} theorem, 44, 72
6.857 + \item {\tt inj_Inl} theorem, 76
6.858 + \item {\tt inj_Inr} theorem, 76
6.859 + \item {\tt inj_onto} constant, 72
6.860 + \item {\tt inj_onto_def} theorem, 72
6.861 + \item {\tt inj_Suc} theorem, 76
6.862 + \item {\tt Inl} constant, 42, 76
6.863 + \item {\tt inl} constant, 110, 115, 125
6.864 + \item {\tt Inl_def} theorem, 42
6.865 + \item {\tt Inl_inject} theorem, 42
6.866 + \item {\tt Inl_neq_Inr} theorem, 42
6.867 + \item {\tt Inl_not_Inr} theorem, 76
6.868 + \item {\tt Inr} constant, 42, 76
6.869 + \item {\tt inr} constant, 110, 115
6.870 + \item {\tt Inr_def} theorem, 42
6.871 + \item {\tt Inr_inject} theorem, 42
6.872 + \item {\tt insert} constant, 65
6.873 + \item {\tt insert_def} theorem, 68
6.874 + \item {\tt insertE} theorem, 70
6.875 + \item {\tt insertI1} theorem, 70
6.876 + \item {\tt insertI2} theorem, 70
6.877 + \item {\tt INT} symbol, 25, 27, 65, 66, 68
6.878 + \item {\tt Int} symbol, 24, 65
6.879 + \item {\tt Int.best_tac}, \bold{9}
6.880 + \item {\tt Int.fast_tac}, \bold{9}, 12
6.881 + \item {\tt Int.inst_step_tac}, \bold{9}
6.882 + \item {\tt Int.safe_step_tac}, \bold{9}
6.883 + \item {\tt Int.safe_tac}, \bold{9}
6.884 + \item {\tt Int.step_tac}, \bold{9}
6.885 + \item {\tt Int_absorb} theorem, 40, 71
6.886 + \item {\tt Int_assoc} theorem, 40, 71
6.887 + \item {\tt Int_commute} theorem, 40, 71
6.888 + \item {\tt INT_D} theorem, 70
6.889 + \item {\tt Int_def} theorem, 29, 68
6.890 + \item {\tt INT_E} theorem, 33, 70
6.891 + \item {\tt Int_greatest} theorem, 35, 51, 53, 71
6.892 + \item {\tt INT_I} theorem, 33, 70
6.893 + \item {\tt Int_Inter_image} theorem, 71
6.894 + \item {\tt Int_lower1} theorem, 35, 52, 71
6.895 + \item {\tt Int_lower2} theorem, 35, 52, 71
6.896 + \item {\tt Int_Un_distrib} theorem, 40, 71
6.897 + \item {\tt Int_Union} theorem, 71
6.898 + \item {\tt Int_Union_RepFun} theorem, 40
6.899 + \item {\tt IntD1} theorem, 34, 70
6.900 + \item {\tt IntD2} theorem, 34, 70
6.901 + \item {\tt IntE} theorem, 34, 52, 70
6.902 + \item {\tt INTER} constant, 65
6.903 + \item {\tt Inter} constant, 24, 65
6.904 + \item {\tt INTER1} constant, 65
6.905 + \item {\tt INTER1_def} theorem, 68
6.906 + \item {\tt INTER_def} theorem, 68
6.907 + \item {\tt Inter_def} theorem, 29, 68
6.908 + \item {\tt Inter_greatest} theorem, 35, 71
6.909 + \item {\tt Inter_lower} theorem, 35, 71
6.910 + \item {\tt Inter_Un_distrib} theorem, 40, 71
6.911 + \item {\tt InterD} theorem, 33, 70
6.912 + \item {\tt InterE} theorem, 33, 70
6.913 + \item {\tt InterI} theorem, 31, 33, 70
6.914 + \item {\tt IntI} theorem, 34, 70
6.915 + \item {\tt intr_rls}, \bold{117}
6.916 + \item {\tt intr_tac}, \bold{118}, 127, 128
6.917 + \item {\tt intrL_rls}, \bold{117}
6.918 + \item {\tt inv} constant, 72
6.919 + \item {\tt inv_def} theorem, 72
6.920
6.921 \indexspace
6.922
6.923 - \item {\ptt lam} symbol, 25, 27, 113
6.924 - \item {\ptt lam_def} theorem, 30
6.925 - \item {\ptt lam_type} theorem, 39
6.926 - \item {\ptt Lambda} constant, 24, 28
6.927 - \item {\ptt lambda} constant, 111, 113
6.928 + \item {\tt lam} symbol, 25, 27, 112
6.929 + \item {\tt lam_def} theorem, 30
6.930 + \item {\tt lam_type} theorem, 38
6.931 + \item {\tt Lambda} constant, 24, 27
6.932 + \item {\tt lambda} constant, 110, 112
6.933 \item $\lambda$-abstractions
6.934 - \subitem in \CTT, 113
6.935 + \subitem in \CTT, 112
6.936 \subitem in \ZF, 25
6.937 - \item {\ptt lamE} theorem, 39, 40
6.938 - \item {\ptt lamI} theorem, 39, 40
6.939 - \item {\ptt LCF} theory, 1
6.940 - \item {\ptt le_cs}, \bold{22}
6.941 - \item {\ptt left_comp_id} theorem, 45
6.942 - \item {\ptt left_comp_inverse} theorem, 45
6.943 - \item {\ptt left_inverse} theorem, 45
6.944 - \item {\ptt length} constant, 48, 80
6.945 - \item {\ptt length_Cons} theorem, 81
6.946 - \item {\ptt length_def} theorem, 48
6.947 - \item {\ptt length_Nil} theorem, 81
6.948 - \item {\ptt less_induct} theorem, 79
6.949 - \item {\ptt less_linear} theorem, 79
6.950 - \item {\ptt less_not_refl} theorem, 79
6.951 - \item {\ptt less_not_sym} theorem, 79
6.952 - \item {\ptt less_trans} theorem, 79
6.953 - \item {\ptt lessI} theorem, 79
6.954 - \item {\ptt Let} constant, 23, 24, 59, 61
6.955 - \item {\ptt let} symbol, 26, 60, 61
6.956 - \item {\ptt Let_def} theorem, 23, 29, 61, 62
6.957 - \item {\ptt lfp_def} theorem, 44
6.958 - \item {\ptt lfp_greatest} theorem, 44
6.959 - \item {\ptt lfp_lowerbound} theorem, 44
6.960 - \item {\ptt lfp_mono} theorem, 44
6.961 - \item {\ptt lfp_subset} theorem, 44
6.962 - \item {\ptt lfp_Tarski} theorem, 44
6.963 - \item {\ptt List} theory, 80, 82
6.964 - \item {\ptt list} constant, 48
6.965 - \item {\ptt list} type, 82, 95
6.966 - \item {\ptt List.induct} theorem, 48
6.967 - \item {\ptt list_all} constant, 80
6.968 - \item {\ptt list_all_Cons} theorem, 81
6.969 - \item {\ptt list_all_Nil} theorem, 81
6.970 - \item {\ptt list_case} constant, 48
6.971 - \item {\ptt list_mono} theorem, 48
6.972 - \item {\ptt list_rec} constant, 48
6.973 - \item {\ptt list_rec_Cons} theorem, 48
6.974 - \item {\ptt list_rec_def} theorem, 48
6.975 - \item {\ptt list_rec_Nil} theorem, 48
6.976 - \item {\ptt LK} theory, 1, 98, 102
6.977 - \item {\ptt LK_dup_pack}, \bold{104}, 106
6.978 - \item {\ptt LK_pack}, \bold{104}
6.979 - \item {\ptt LList} theory, 95
6.980 - \item {\ptt logic} class, 4
6.981 + \item {\tt lamE} theorem, 38, 39
6.982 + \item {\tt lamI} theorem, 38, 39
6.983 + \item {\tt LCF} theory, 1
6.984 + \item {\tt le_cs}, \bold{22}
6.985 + \item {\tt LEAST} constant, 59, 60, 75
6.986 + \item {\tt Least} constant, 58
6.987 + \item {\tt Least_def} theorem, 62
6.988 + \item {\tt left_comp_id} theorem, 44
6.989 + \item {\tt left_comp_inverse} theorem, 44
6.990 + \item {\tt left_inverse} theorem, 44
6.991 + \item {\tt length} constant, 48, 79
6.992 + \item {\tt length_def} theorem, 48
6.993 + \item {\tt less_induct} theorem, 77
6.994 + \item {\tt Let} constant, 23, 24, 58, 61
6.995 + \item {\tt let} symbol, 26, 59, 61
6.996 + \item {\tt Let_def} theorem, 23, 29, 61, 62
6.997 + \item {\tt lfp_def} theorem, 43
6.998 + \item {\tt lfp_greatest} theorem, 43
6.999 + \item {\tt lfp_lowerbound} theorem, 43
6.1000 + \item {\tt lfp_mono} theorem, 43
6.1001 + \item {\tt lfp_subset} theorem, 43
6.1002 + \item {\tt lfp_Tarski} theorem, 43
6.1003 + \item {\tt List} theory, 78, 79
6.1004 + \item {\tt list} constant, 48
6.1005 + \item {\tt list} type, 78, 94
6.1006 + \item {\tt List.induct} theorem, 48
6.1007 + \item {\tt list_all} constant, 79
6.1008 + \item {\tt list_case} constant, 48
6.1009 + \item {\tt list_mono} theorem, 48
6.1010 + \item {\tt list_rec} constant, 48
6.1011 + \item {\tt list_rec_Cons} theorem, 48
6.1012 + \item {\tt list_rec_def} theorem, 48
6.1013 + \item {\tt list_rec_Nil} theorem, 48
6.1014 + \item {\tt LK} theory, 1, 97, 101
6.1015 + \item {\tt LK_dup_pack}, \bold{103}, 105
6.1016 + \item {\tt LK_pack}, \bold{103}
6.1017 + \item {\tt LList} theory, 94
6.1018 + \item {\tt logic} class, 4
6.1019
6.1020 \indexspace
6.1021
6.1022 - \item {\ptt map} constant, 48, 80
6.1023 - \item {\ptt map_app_distrib} theorem, 48
6.1024 - \item {\ptt map_compose} theorem, 48
6.1025 - \item {\ptt map_Cons} theorem, 81
6.1026 - \item {\ptt map_def} theorem, 48
6.1027 - \item {\ptt map_flat} theorem, 48
6.1028 - \item {\ptt map_ident} theorem, 48
6.1029 - \item {\ptt map_Nil} theorem, 81
6.1030 - \item {\ptt map_type} theorem, 48
6.1031 - \item {\ptt max} constant, 58
6.1032 - \item {\ptt mem} symbol, 80
6.1033 - \item {\ptt mem_asym} theorem, 34, 35
6.1034 - \item {\ptt mem_Collect_eq} theorem, 69
6.1035 - \item {\ptt mem_Cons} theorem, 81
6.1036 - \item {\ptt mem_irrefl} theorem, 34
6.1037 - \item {\ptt mem_Nil} theorem, 81
6.1038 - \item {\ptt min} constant, 58
6.1039 - \item {\ptt minus} class, 58
6.1040 - \item {\ptt mod} symbol, 46, 78, 122
6.1041 - \item {\ptt mod_def} theorem, 46, 122
6.1042 - \item {\ptt mod_geq} theorem, 79
6.1043 - \item {\ptt mod_less} theorem, 79
6.1044 - \item {\ptt mod_quo_equality} theorem, 46
6.1045 - \item {\ptt Modal} theory, 1
6.1046 - \item {\ptt mono} constant, 58, 66
6.1047 - \item {\ptt mono_def} theorem, 69
6.1048 - \item {\ptt monoD} theorem, 72
6.1049 - \item {\ptt monoI} theorem, 72
6.1050 - \item {\ptt mp} theorem, 7, 62
6.1051 - \item {\ptt mp_tac}, \bold{9}, \bold{121}
6.1052 - \item {\ptt mult_0} theorem, 46
6.1053 - \item {\ptt mult_assoc} theorem, 46, 122
6.1054 - \item {\ptt mult_commute} theorem, 46, 122
6.1055 - \item {\ptt mult_def} theorem, 46, 79, 122
6.1056 - \item {\ptt mult_Suc} theorem, 79
6.1057 - \item {\ptt mult_succ} theorem, 46
6.1058 - \item {\ptt mult_type} theorem, 46
6.1059 - \item {\ptt mult_typing} theorem, 122
6.1060 - \item {\ptt multC0} theorem, 122
6.1061 - \item {\ptt multC_succ} theorem, 122
6.1062 + \item {\tt map} constant, 48, 79
6.1063 + \item {\tt map_app_distrib} theorem, 48
6.1064 + \item {\tt map_compose} theorem, 48
6.1065 + \item {\tt map_def} theorem, 48
6.1066 + \item {\tt map_flat} theorem, 48
6.1067 + \item {\tt map_ident} theorem, 48
6.1068 + \item {\tt map_type} theorem, 48
6.1069 + \item {\tt max} constant, 59, 75
6.1070 + \item {\tt mem} symbol, 79
6.1071 + \item {\tt mem_asym} theorem, 34, 35
6.1072 + \item {\tt mem_Collect_eq} theorem, 68
6.1073 + \item {\tt mem_irrefl} theorem, 34
6.1074 + \item {\tt min} constant, 59, 75
6.1075 + \item {\tt minus} class, 59
6.1076 + \item {\tt mod} symbol, 46, 76, 121
6.1077 + \item {\tt mod_def} theorem, 46, 121
6.1078 + \item {\tt mod_geq} theorem, 77
6.1079 + \item {\tt mod_less} theorem, 77
6.1080 + \item {\tt mod_quo_equality} theorem, 46
6.1081 + \item {\tt Modal} theory, 1
6.1082 + \item {\tt mono} constant, 59
6.1083 + \item {\tt mp} theorem, 7, 61
6.1084 + \item {\tt mp_tac}, \bold{9}, \bold{119}
6.1085 + \item {\tt mult_0} theorem, 46
6.1086 + \item {\tt mult_assoc} theorem, 46, 121
6.1087 + \item {\tt mult_commute} theorem, 46, 121
6.1088 + \item {\tt mult_def} theorem, 46, 121
6.1089 + \item {\tt mult_succ} theorem, 46
6.1090 + \item {\tt mult_type} theorem, 46
6.1091 + \item {\tt mult_typing} theorem, 121
6.1092 + \item {\tt multC0} theorem, 121
6.1093 + \item {\tt multC_succ} theorem, 121
6.1094
6.1095 \indexspace
6.1096
6.1097 - \item {\ptt N} constant, 111
6.1098 - \item {\ptt n_not_Suc_n} theorem, 78
6.1099 - \item {\ptt Nat} theory, 43, 77
6.1100 - \item {\ptt nat} constant, 46
6.1101 - \item {\ptt nat} type, 77
6.1102 - \item {\ptt nat_0I} theorem, 46
6.1103 - \item {\ptt nat_case} constant, 46, 78
6.1104 - \item {\ptt nat_case_0} theorem, 46, 79
6.1105 - \item {\ptt nat_case_def} theorem, 46
6.1106 - \item {\ptt nat_case_Suc} theorem, 79
6.1107 - \item {\ptt nat_case_succ} theorem, 46
6.1108 - \item {\ptt nat_def} theorem, 46
6.1109 - \item {\ptt nat_ind_tac}, 77
6.1110 - \item {\ptt nat_induct} theorem, 46, 78
6.1111 - \item {\ptt nat_rec} constant, 78
6.1112 - \item {\ptt nat_rec_0} theorem, 79
6.1113 - \item {\ptt nat_rec_Suc} theorem, 79
6.1114 - \item {\ptt nat_succI} theorem, 46
6.1115 - \item {\ptt NC0} theorem, 115
6.1116 - \item {\ptt NC_succ} theorem, 115
6.1117 - \item {\ptt NE} theorem, 115, 116, 124
6.1118 - \item {\ptt NEL} theorem, 115
6.1119 - \item {\ptt NF} theorem, 115, 124
6.1120 - \item {\ptt NI0} theorem, 115
6.1121 - \item {\ptt NI_succ} theorem, 115
6.1122 - \item {\ptt NI_succL} theorem, 115
6.1123 - \item {\ptt Nil_Cons_iff} theorem, 48
6.1124 - \item {\ptt NilI} theorem, 48
6.1125 - \item {\ptt NIO} theorem, 124
6.1126 - \item {\ptt Not} constant, 6, 99
6.1127 - \item {\ptt not} constant, 59
6.1128 - \item {\ptt not_def} theorem, 7, 42, 62
6.1129 - \item {\ptt not_impE} theorem, 8
6.1130 - \item {\ptt not_less0} theorem, 79
6.1131 - \item {\ptt not_sym} theorem, 64
6.1132 - \item {\ptt notE} theorem, 8, 9, 64
6.1133 - \item {\ptt notI} theorem, 8, 64
6.1134 - \item {\ptt notL} theorem, 101
6.1135 - \item {\ptt notnotD} theorem, 10, 65
6.1136 - \item {\ptt notR} theorem, 101
6.1137 - \item {\ptt null} constant, 80
6.1138 - \item {\ptt null_Cons} theorem, 81
6.1139 - \item {\ptt null_Nil} theorem, 81
6.1140 + \item {\tt N} constant, 110
6.1141 + \item {\tt n_not_Suc_n} theorem, 76
6.1142 + \item {\tt Nat} theory, 45, 75
6.1143 + \item {\tt nat} constant, 46
6.1144 + \item {\tt nat} type, 75
6.1145 + \item {\tt nat_0I} theorem, 46
6.1146 + \item {\tt nat_case} constant, 46
6.1147 + \item {\tt nat_case_0} theorem, 46
6.1148 + \item {\tt nat_case_def} theorem, 46
6.1149 + \item {\tt nat_case_succ} theorem, 46
6.1150 + \item {\tt nat_def} theorem, 46
6.1151 + \item {\tt nat_induct} theorem, 46, 76
6.1152 + \item {\tt nat_rec} constant, 77
6.1153 + \item {\tt nat_succI} theorem, 46
6.1154 + \item {\tt NatDef} theory, 75
6.1155 + \item {\tt NC0} theorem, 114
6.1156 + \item {\tt NC_succ} theorem, 114
6.1157 + \item {\tt NE} theorem, 113, 114, 122
6.1158 + \item {\tt NEL} theorem, 114
6.1159 + \item {\tt NF} theorem, 114, 123
6.1160 + \item {\tt NI0} theorem, 114
6.1161 + \item {\tt NI_succ} theorem, 114
6.1162 + \item {\tt NI_succL} theorem, 114
6.1163 + \item {\tt Nil_Cons_iff} theorem, 48
6.1164 + \item {\tt NilI} theorem, 48
6.1165 + \item {\tt NIO} theorem, 122
6.1166 + \item {\tt Not} constant, 6, 58, 98
6.1167 + \item {\tt not_def} theorem, 7, 41, 62
6.1168 + \item {\tt not_impE} theorem, 8
6.1169 + \item {\tt not_sym} theorem, 63
6.1170 + \item {\tt notE} theorem, 8, 9, 63
6.1171 + \item {\tt notI} theorem, 8, 63
6.1172 + \item {\tt notL} theorem, 100
6.1173 + \item {\tt notnotD} theorem, 10, 64
6.1174 + \item {\tt notR} theorem, 100
6.1175 + \item {\tt nth} constant, 79
6.1176 + \item {\tt null} constant, 79
6.1177
6.1178 \indexspace
6.1179
6.1180 - \item {\ptt O} symbol, 45
6.1181 - \item {\ptt o} symbol, 59, 72
6.1182 - \item {\ptt o} type, 4, 98
6.1183 - \item {\ptt o_def} theorem, 62
6.1184 - \item {\ptt of} symbol, 61
6.1185 - \item {\ptt or_def} theorem, 42, 62
6.1186 - \item {\ptt ord} class, 58, 77
6.1187 + \item {\tt O} symbol, 44
6.1188 + \item {\tt o} symbol, 58, 72
6.1189 + \item {\tt o} type, 4, 97
6.1190 + \item {\tt o_def} theorem, 62
6.1191 + \item {\tt of} symbol, 61
6.1192 + \item {\tt or_def} theorem, 41, 62
6.1193 + \item {\tt Ord} theory, 59
6.1194 + \item {\tt ord} class, 59, 60, 75
6.1195 + \item {\tt order} class, 59
6.1196
6.1197 \indexspace
6.1198
6.1199 - \item {\ptt pack} ML type, 104
6.1200 - \item {\ptt Pair} constant, 24, 25, 75
6.1201 - \item {\ptt pair} constant, 111
6.1202 - \item {\ptt Pair_def} theorem, 30
6.1203 - \item {\ptt Pair_eq} theorem, 75
6.1204 - \item {\ptt Pair_inject} theorem, 36, 75
6.1205 - \item {\ptt Pair_inject1} theorem, 36
6.1206 - \item {\ptt Pair_inject2} theorem, 36
6.1207 - \item {\ptt Pair_neq_0} theorem, 36
6.1208 - \item {\ptt PairE} theorem, 75
6.1209 - \item {\ptt pairing} theorem, 33
6.1210 - \item {\ptt pc_tac}, \bold{105}, \bold{121}, 127--129
6.1211 - \item {\ptt Perm} theory, 43
6.1212 - \item {\ptt Pi} constant, 24, 27, 40
6.1213 - \item {\ptt Pi_def} theorem, 30
6.1214 - \item {\ptt Pi_type} theorem, 38, 40
6.1215 - \item {\ptt plus} class, 58
6.1216 - \item {\ptt PlusC_inl} theorem, 117
6.1217 - \item {\ptt PlusC_inr} theorem, 117
6.1218 - \item {\ptt PlusE} theorem, 117, 121, 126
6.1219 - \item {\ptt PlusEL} theorem, 117
6.1220 - \item {\ptt PlusF} theorem, 117
6.1221 - \item {\ptt PlusFL} theorem, 117
6.1222 - \item {\ptt PlusI_inl} theorem, 117, 126
6.1223 - \item {\ptt PlusI_inlL} theorem, 117
6.1224 - \item {\ptt PlusI_inr} theorem, 117
6.1225 - \item {\ptt PlusI_inrL} theorem, 117
6.1226 - \item {\ptt Pow} constant, 24, 66
6.1227 - \item {\ptt Pow_def} theorem, 69
6.1228 - \item {\ptt Pow_iff} theorem, 29
6.1229 - \item {\ptt Pow_mono} theorem, 51
6.1230 - \item {\ptt PowD} theorem, 32, 53, 71
6.1231 - \item {\ptt PowI} theorem, 32, 53, 71
6.1232 - \item primitive recursion, 90--91
6.1233 - \item {\ptt primrec}, 90--91
6.1234 - \item {\ptt PrimReplace} constant, 24, 28
6.1235 + \item {\tt pack} ML type, 103
6.1236 + \item {\tt Pair} constant, 24, 25, 74
6.1237 + \item {\tt pair} constant, 110
6.1238 + \item {\tt Pair_def} theorem, 30
6.1239 + \item {\tt Pair_eq} theorem, 74
6.1240 + \item {\tt Pair_inject} theorem, 36, 74
6.1241 + \item {\tt Pair_inject1} theorem, 36
6.1242 + \item {\tt Pair_inject2} theorem, 36
6.1243 + \item {\tt Pair_neq_0} theorem, 36
6.1244 + \item {\tt PairE} theorem, 74
6.1245 + \item {\tt pairing} theorem, 33
6.1246 + \item {\tt pc_tac}, \bold{104}, \bold{120}, 126, 127
6.1247 + \item {\tt Perm} theory, 41
6.1248 + \item {\tt Pi} constant, 24, 27, 39
6.1249 + \item {\tt Pi_def} theorem, 30
6.1250 + \item {\tt Pi_type} theorem, 38, 39
6.1251 + \item {\tt plus} class, 59
6.1252 + \item {\tt PlusC_inl} theorem, 116
6.1253 + \item {\tt PlusC_inr} theorem, 116
6.1254 + \item {\tt PlusE} theorem, 116, 120, 124
6.1255 + \item {\tt PlusEL} theorem, 116
6.1256 + \item {\tt PlusF} theorem, 116
6.1257 + \item {\tt PlusFL} theorem, 116
6.1258 + \item {\tt PlusI_inl} theorem, 116, 125
6.1259 + \item {\tt PlusI_inlL} theorem, 116
6.1260 + \item {\tt PlusI_inr} theorem, 116
6.1261 + \item {\tt PlusI_inrL} theorem, 116
6.1262 + \item {\tt Pow} constant, 24, 65
6.1263 + \item {\tt Pow_def} theorem, 68
6.1264 + \item {\tt Pow_iff} theorem, 29
6.1265 + \item {\tt Pow_mono} theorem, 51
6.1266 + \item {\tt PowD} theorem, 32, 52, 70
6.1267 + \item {\tt PowI} theorem, 32, 52, 70
6.1268 + \item primitive recursion, 88--90
6.1269 + \item {\tt primrec}, 88--90
6.1270 + \item {\tt primrec} symbol, 77
6.1271 + \item {\tt PrimReplace} constant, 24, 28
6.1272 \item priorities, 2
6.1273 - \item {\ptt PROD} symbol, 25, 27, 112, 113
6.1274 - \item {\ptt Prod} constant, 111
6.1275 - \item {\ptt Prod} theory, 75
6.1276 - \item {\ptt ProdC} theorem, 115, 131
6.1277 - \item {\ptt ProdC2} theorem, 115
6.1278 - \item {\ptt ProdE} theorem, 115, 129, 130, 132
6.1279 - \item {\ptt ProdEL} theorem, 115
6.1280 - \item {\ptt ProdF} theorem, 115
6.1281 - \item {\ptt ProdFL} theorem, 115
6.1282 - \item {\ptt ProdI} theorem, 115, 121, 124
6.1283 - \item {\ptt ProdIL} theorem, 115
6.1284 - \item {\ptt prop_cs}, \bold{10}, \bold{75}
6.1285 - \item {\ptt prop_pack}, \bold{104}
6.1286 + \item {\tt PROD} symbol, 25, 27, 111, 112
6.1287 + \item {\tt Prod} constant, 110
6.1288 + \item {\tt Prod} theory, 74
6.1289 + \item {\tt ProdC} theorem, 114, 130
6.1290 + \item {\tt ProdC2} theorem, 114
6.1291 + \item {\tt ProdE} theorem, 114, 127, 129, 131
6.1292 + \item {\tt ProdEL} theorem, 114
6.1293 + \item {\tt ProdF} theorem, 114
6.1294 + \item {\tt ProdFL} theorem, 114
6.1295 + \item {\tt ProdI} theorem, 114, 120, 122
6.1296 + \item {\tt ProdIL} theorem, 114
6.1297 + \item {\tt prop_cs}, \bold{10}, \bold{73}
6.1298 + \item {\tt prop_pack}, \bold{103}
6.1299
6.1300 \indexspace
6.1301
6.1302 - \item {\ptt qcase_def} theorem, 43
6.1303 - \item {\ptt qconverse} constant, 40
6.1304 - \item {\ptt qconverse_def} theorem, 43
6.1305 - \item {\ptt qfsplit_def} theorem, 43
6.1306 - \item {\ptt QInl_def} theorem, 43
6.1307 - \item {\ptt QInr_def} theorem, 43
6.1308 - \item {\ptt QPair} theory, 40
6.1309 - \item {\ptt QPair_def} theorem, 43
6.1310 - \item {\ptt QSigma} constant, 40
6.1311 - \item {\ptt QSigma_def} theorem, 43
6.1312 - \item {\ptt qsplit} constant, 40
6.1313 - \item {\ptt qsplit_def} theorem, 43
6.1314 - \item {\ptt qsum_def} theorem, 43
6.1315 - \item {\ptt QUniv} theory, 43
6.1316 + \item {\tt qcase_def} theorem, 42
6.1317 + \item {\tt qconverse} constant, 41
6.1318 + \item {\tt qconverse_def} theorem, 42
6.1319 + \item {\tt qfsplit_def} theorem, 42
6.1320 + \item {\tt QInl_def} theorem, 42
6.1321 + \item {\tt QInr_def} theorem, 42
6.1322 + \item {\tt QPair} theory, 41
6.1323 + \item {\tt QPair_def} theorem, 42
6.1324 + \item {\tt QSigma} constant, 41
6.1325 + \item {\tt QSigma_def} theorem, 42
6.1326 + \item {\tt qsplit} constant, 41
6.1327 + \item {\tt qsplit_def} theorem, 42
6.1328 + \item {\tt qsum_def} theorem, 42
6.1329 + \item {\tt QUniv} theory, 45
6.1330
6.1331 \indexspace
6.1332
6.1333 - \item {\ptt range} constant, 24, 66, 96
6.1334 - \item {\ptt range_def} theorem, 30, 69
6.1335 - \item {\ptt range_of_fun} theorem, 38, 40
6.1336 - \item {\ptt range_subset} theorem, 37
6.1337 - \item {\ptt range_type} theorem, 38
6.1338 - \item {\ptt rangeE} theorem, 37, 72, 96
6.1339 - \item {\ptt rangeI} theorem, 37, 72
6.1340 - \item {\ptt rank} constant, 47
6.1341 - \item {\ptt rank_ss}, \bold{22}
6.1342 - \item {\ptt rec} constant, 46, 111, 116
6.1343 - \item {\ptt rec_0} theorem, 46
6.1344 - \item {\ptt rec_def} theorem, 46
6.1345 - \item {\ptt rec_succ} theorem, 46
6.1346 - \item {\ptt red_if_equal} theorem, 114
6.1347 - \item {\ptt Reduce} constant, 111, 116, 120
6.1348 - \item {\ptt refl} theorem, 7, 62, 101
6.1349 - \item {\ptt refl_elem} theorem, 114, 119
6.1350 - \item {\ptt refl_red} theorem, 114
6.1351 - \item {\ptt refl_type} theorem, 114, 119
6.1352 - \item {\ptt REPEAT_FIRST}, 119
6.1353 - \item {\ptt repeat_goal_tac}, \bold{105}
6.1354 - \item {\ptt RepFun} constant, 24, 27, 28, 31
6.1355 - \item {\ptt RepFun_def} theorem, 29
6.1356 - \item {\ptt RepFunE} theorem, 33
6.1357 - \item {\ptt RepFunI} theorem, 33
6.1358 - \item {\ptt Replace} constant, 24, 27, 28, 31
6.1359 - \item {\ptt Replace_def} theorem, 29
6.1360 - \item {\ptt replace_type} theorem, 118, 131
6.1361 - \item {\ptt ReplaceE} theorem, 33
6.1362 - \item {\ptt ReplaceI} theorem, 33
6.1363 - \item {\ptt replacement} theorem, 29
6.1364 - \item {\ptt reresolve_tac}, \bold{105}
6.1365 - \item {\ptt res_inst_tac}, 63
6.1366 - \item {\ptt restrict} constant, 24, 31
6.1367 - \item {\ptt restrict} theorem, 38
6.1368 - \item {\ptt restrict_bij} theorem, 45
6.1369 - \item {\ptt restrict_def} theorem, 30
6.1370 - \item {\ptt restrict_type} theorem, 38
6.1371 - \item {\ptt rev} constant, 48, 80
6.1372 - \item {\ptt rev_Cons} theorem, 81
6.1373 - \item {\ptt rev_def} theorem, 48
6.1374 - \item {\ptt rev_Nil} theorem, 81
6.1375 - \item {\ptt rew_tac}, 17, \bold{120}
6.1376 - \item {\ptt rewrite_rule}, 18
6.1377 - \item {\ptt right_comp_id} theorem, 45
6.1378 - \item {\ptt right_comp_inverse} theorem, 45
6.1379 - \item {\ptt right_inverse} theorem, 45
6.1380 - \item {\ptt RL}, 126
6.1381 - \item {\ptt RS}, 130, 132
6.1382 + \item {\tt range} constant, 24, 65, 95
6.1383 + \item {\tt range_def} theorem, 30, 68
6.1384 + \item {\tt range_of_fun} theorem, 38, 39
6.1385 + \item {\tt range_subset} theorem, 37
6.1386 + \item {\tt range_type} theorem, 38
6.1387 + \item {\tt rangeE} theorem, 37, 70, 95
6.1388 + \item {\tt rangeI} theorem, 37, 70
6.1389 + \item {\tt rank} constant, 47
6.1390 + \item {\tt rank_ss}, \bold{22}
6.1391 + \item {\tt rec} constant, 46, 110, 113
6.1392 + \item {\tt rec_0} theorem, 46
6.1393 + \item {\tt rec_def} theorem, 46
6.1394 + \item {\tt rec_succ} theorem, 46
6.1395 + \item {\tt red_if_equal} theorem, 113
6.1396 + \item {\tt Reduce} constant, 110, 113, 119
6.1397 + \item {\tt refl} theorem, 7, 61, 100
6.1398 + \item {\tt refl_elem} theorem, 113, 117
6.1399 + \item {\tt refl_red} theorem, 113
6.1400 + \item {\tt refl_type} theorem, 113, 117
6.1401 + \item {\tt REPEAT_FIRST}, 118
6.1402 + \item {\tt repeat_goal_tac}, \bold{104}
6.1403 + \item {\tt RepFun} constant, 24, 27, 28, 31
6.1404 + \item {\tt RepFun_def} theorem, 29
6.1405 + \item {\tt RepFunE} theorem, 33
6.1406 + \item {\tt RepFunI} theorem, 33
6.1407 + \item {\tt Replace} constant, 24, 27, 28, 31
6.1408 + \item {\tt Replace_def} theorem, 29
6.1409 + \item {\tt replace_type} theorem, 117, 129
6.1410 + \item {\tt ReplaceE} theorem, 33
6.1411 + \item {\tt ReplaceI} theorem, 33
6.1412 + \item {\tt replacement} theorem, 29
6.1413 + \item {\tt reresolve_tac}, \bold{104}
6.1414 + \item {\tt res_inst_tac}, 60
6.1415 + \item {\tt restrict} constant, 24, 31
6.1416 + \item {\tt restrict} theorem, 38
6.1417 + \item {\tt restrict_bij} theorem, 44
6.1418 + \item {\tt restrict_def} theorem, 30
6.1419 + \item {\tt restrict_type} theorem, 38
6.1420 + \item {\tt rev} constant, 48, 79
6.1421 + \item {\tt rev_def} theorem, 48
6.1422 + \item {\tt rew_tac}, 17, \bold{119}
6.1423 + \item {\tt rewrite_rule}, 18
6.1424 + \item {\tt right_comp_id} theorem, 44
6.1425 + \item {\tt right_comp_inverse} theorem, 44
6.1426 + \item {\tt right_inverse} theorem, 44
6.1427 + \item {\tt RL}, 124
6.1428 + \item {\tt RS}, 129, 131
6.1429
6.1430 \indexspace
6.1431
6.1432 - \item {\ptt safe_goal_tac}, \bold{106}
6.1433 - \item {\ptt safe_tac}, \bold{121}
6.1434 - \item {\ptt safestep_tac}, \bold{121}
6.1435 + \item {\tt safe_goal_tac}, \bold{105}
6.1436 + \item {\tt safe_tac}, \bold{120}
6.1437 + \item {\tt safestep_tac}, \bold{120}
6.1438 \item search
6.1439 - \subitem best-first, 97
6.1440 - \item {\ptt select_equality} theorem, 63, 65
6.1441 - \item {\ptt selectI} theorem, 62, 63
6.1442 - \item {\ptt separation} theorem, 33
6.1443 - \item {\ptt Seqof} constant, 99
6.1444 - \item sequent calculus, 98--109
6.1445 - \item {\ptt Set} theory, 68, 69
6.1446 - \item {\ptt set} type, 68
6.1447 - \item set theory, 22--57
6.1448 - \item {\ptt set_cs}, \bold{75}, 97
6.1449 - \item {\ptt set_diff_def} theorem, 69
6.1450 - \item {\ptt show_sorts}, 63
6.1451 - \item {\ptt show_types}, 63
6.1452 - \item {\ptt Sigma} constant, 24, 27, 28, 36, 75
6.1453 - \item {\ptt Sigma_def} theorem, 30, 75
6.1454 - \item {\ptt SigmaE} theorem, 36, 75
6.1455 - \item {\ptt SigmaE2} theorem, 36
6.1456 - \item {\ptt SigmaI} theorem, 36, 75
6.1457 + \subitem best-first, 96
6.1458 + \item {\tt select_equality} theorem, 61, 64
6.1459 + \item {\tt selectI} theorem, 61
6.1460 + \item {\tt separation} theorem, 33
6.1461 + \item {\tt Seqof} constant, 98
6.1462 + \item sequent calculus, 97--108
6.1463 + \item {\tt Set} theory, 67, 68
6.1464 + \item {\tt set} type, 67
6.1465 + \item set theory, 22--56
6.1466 + \item {\tt set_current_thy}, 96
6.1467 + \item {\tt set_diff_def} theorem, 68
6.1468 + \item {\tt set_of_list} constant, 79
6.1469 + \item {\tt show_sorts}, 60
6.1470 + \item {\tt show_types}, 60
6.1471 + \item {\tt Sigma} constant, 24, 27, 28, 36, 74
6.1472 + \item {\tt Sigma_def} theorem, 30, 74
6.1473 + \item {\tt SigmaE} theorem, 36, 74
6.1474 + \item {\tt SigmaE2} theorem, 36
6.1475 + \item {\tt SigmaI} theorem, 36, 74
6.1476 \item simplification
6.1477 - \subitem of conjunctions, 74
6.1478 - \item {\ptt singletonE} theorem, 34
6.1479 - \item {\ptt singletonI} theorem, 34
6.1480 - \item {\ptt snd} constant, 24, 31, 75, 111, 118
6.1481 - \item {\ptt snd_conv} theorem, 36, 75
6.1482 - \item {\ptt snd_def} theorem, 30, 116
6.1483 - \item {\ptt sobj} type, 100
6.1484 - \item {\ptt spec} theorem, 7, 65
6.1485 - \item {\ptt split} constant, 24, 31, 75, 111, 126
6.1486 - \item {\ptt split} theorem, 36, 75
6.1487 - \item {\ptt split_all_tac}, \bold{76}
6.1488 - \item {\ptt split_def} theorem, 30
6.1489 - \item {\ptt ssubst} theorem, 8, 63, 64
6.1490 - \item {\ptt stac}, \bold{74}
6.1491 - \item {\ptt step_tac}, 21, \bold{106}, \bold{121}
6.1492 - \item {\ptt strip_tac}, \bold{63}
6.1493 - \item {\ptt subset_def} theorem, 29, 69
6.1494 - \item {\ptt subset_refl} theorem, 32, 70
6.1495 - \item {\ptt subset_trans} theorem, 32, 70
6.1496 - \item {\ptt subsetCE} theorem, 32, 70, 72
6.1497 - \item {\ptt subsetD} theorem, 32, 55, 70, 72
6.1498 - \item {\ptt subsetI} theorem, 32, 52, 54, 70
6.1499 - \item {\ptt subst} theorem, 7, 62
6.1500 - \item {\ptt subst_elem} theorem, 114
6.1501 - \item {\ptt subst_elemL} theorem, 114
6.1502 - \item {\ptt subst_eqtyparg} theorem, 118, 131
6.1503 - \item {\ptt subst_prodE} theorem, 118
6.1504 - \item {\ptt subst_type} theorem, 114
6.1505 - \item {\ptt subst_typeL} theorem, 114
6.1506 - \item {\ptt Suc} constant, 78
6.1507 - \item {\ptt Suc_less_eq} theorem, 79
6.1508 - \item {\ptt Suc_not_Zero} theorem, 78
6.1509 - \item {\ptt succ} constant, 24, 28, 111
6.1510 - \item {\ptt succ_def} theorem, 30
6.1511 - \item {\ptt succ_inject} theorem, 34
6.1512 - \item {\ptt succ_neq_0} theorem, 34
6.1513 - \item {\ptt succCI} theorem, 34
6.1514 - \item {\ptt succE} theorem, 34
6.1515 - \item {\ptt succI1} theorem, 34
6.1516 - \item {\ptt succI2} theorem, 34
6.1517 - \item {\ptt SUM} symbol, 25, 27, 112, 113
6.1518 - \item {\ptt Sum} constant, 111
6.1519 - \item {\ptt Sum} theory, 40, 76
6.1520 - \item {\ptt sum_case} constant, 77
6.1521 - \item {\ptt sum_case_Inl} theorem, 77
6.1522 - \item {\ptt sum_case_Inr} theorem, 77
6.1523 - \item {\ptt sum_def} theorem, 42
6.1524 - \item {\ptt sum_InlI} theorem, 42
6.1525 - \item {\ptt sum_InrI} theorem, 42
6.1526 - \item {\ptt SUM_Int_distrib1} theorem, 41
6.1527 - \item {\ptt SUM_Int_distrib2} theorem, 41
6.1528 - \item {\ptt SUM_Un_distrib1} theorem, 41
6.1529 - \item {\ptt SUM_Un_distrib2} theorem, 41
6.1530 - \item {\ptt SumC} theorem, 116
6.1531 - \item {\ptt SumE} theorem, 116, 121, 126
6.1532 - \item {\ptt sumE} theorem, 77
6.1533 - \item {\ptt sumE2} theorem, 42
6.1534 - \item {\ptt SumE_fst} theorem, 118, 130, 132
6.1535 - \item {\ptt SumE_snd} theorem, 118, 132
6.1536 - \item {\ptt SumEL} theorem, 116
6.1537 - \item {\ptt SumF} theorem, 116
6.1538 - \item {\ptt SumFL} theorem, 116
6.1539 - \item {\ptt SumI} theorem, 116, 127
6.1540 - \item {\ptt SumIL} theorem, 116
6.1541 - \item {\ptt SumIL2} theorem, 118
6.1542 - \item {\ptt surj} constant, 45, 66, 72
6.1543 - \item {\ptt surj_def} theorem, 45, 69
6.1544 - \item {\ptt surjective_pairing} theorem, 75
6.1545 - \item {\ptt surjective_sum} theorem, 77
6.1546 - \item {\ptt swap} theorem, 10, 65
6.1547 - \item {\ptt swap_res_tac}, 15, 97
6.1548 - \item {\ptt sym} theorem, 8, 64, 101
6.1549 - \item {\ptt sym_elem} theorem, 114
6.1550 - \item {\ptt sym_type} theorem, 114
6.1551 - \item {\ptt symL} theorem, 102
6.1552 + \subitem of conjunctions, 73
6.1553 + \item {\tt singletonE} theorem, 34
6.1554 + \item {\tt singletonI} theorem, 34
6.1555 + \item {\tt snd} constant, 24, 28, 74, 110, 115
6.1556 + \item {\tt snd_conv} theorem, 36, 74
6.1557 + \item {\tt snd_def} theorem, 30, 115
6.1558 + \item {\tt sobj} type, 99
6.1559 + \item {\tt spec} theorem, 7, 64
6.1560 + \item {\tt split} constant, 24, 28, 74, 110, 124
6.1561 + \item {\tt split} theorem, 36, 74
6.1562 + \item {\tt split_all_tac}, \bold{75}
6.1563 + \item {\tt split_def} theorem, 30
6.1564 + \item {\tt ssubst} theorem, 8, 62, 63
6.1565 + \item {\tt stac}, \bold{73}
6.1566 + \item {\tt step_tac}, 21, \bold{105}, \bold{120}
6.1567 + \item {\tt strip_tac}, \bold{62}
6.1568 + \item {\tt subset_def} theorem, 29, 68
6.1569 + \item {\tt subset_refl} theorem, 32, 69
6.1570 + \item {\tt subset_trans} theorem, 32, 69
6.1571 + \item {\tt subsetCE} theorem, 32, 69, 72
6.1572 + \item {\tt subsetD} theorem, 32, 54, 69, 72
6.1573 + \item {\tt subsetI} theorem, 32, 52, 53, 69
6.1574 + \item {\tt subst} theorem, 7, 61
6.1575 + \item {\tt subst_elem} theorem, 113
6.1576 + \item {\tt subst_elemL} theorem, 113
6.1577 + \item {\tt subst_eqtyparg} theorem, 117, 129
6.1578 + \item {\tt subst_prodE} theorem, 115, 117
6.1579 + \item {\tt subst_type} theorem, 113
6.1580 + \item {\tt subst_typeL} theorem, 113
6.1581 + \item {\tt Suc} constant, 76
6.1582 + \item {\tt Suc_not_Zero} theorem, 76
6.1583 + \item {\tt succ} constant, 24, 28, 110
6.1584 + \item {\tt succ_def} theorem, 30
6.1585 + \item {\tt succ_inject} theorem, 34
6.1586 + \item {\tt succ_neq_0} theorem, 34
6.1587 + \item {\tt succCI} theorem, 34
6.1588 + \item {\tt succE} theorem, 34
6.1589 + \item {\tt succI1} theorem, 34
6.1590 + \item {\tt succI2} theorem, 34
6.1591 + \item {\tt SUM} symbol, 25, 27, 111, 112
6.1592 + \item {\tt Sum} constant, 110
6.1593 + \item {\tt Sum} theory, 41, 75
6.1594 + \item {\tt sum_case} constant, 76
6.1595 + \item {\tt sum_case_Inl} theorem, 76
6.1596 + \item {\tt sum_case_Inr} theorem, 76
6.1597 + \item {\tt sum_def} theorem, 42
6.1598 + \item {\tt sum_InlI} theorem, 42
6.1599 + \item {\tt sum_InrI} theorem, 42
6.1600 + \item {\tt SUM_Int_distrib1} theorem, 40
6.1601 + \item {\tt SUM_Int_distrib2} theorem, 40
6.1602 + \item {\tt SUM_Un_distrib1} theorem, 40
6.1603 + \item {\tt SUM_Un_distrib2} theorem, 40
6.1604 + \item {\tt SumC} theorem, 115
6.1605 + \item {\tt SumE} theorem, 115, 120, 124
6.1606 + \item {\tt sumE} theorem, 76
6.1607 + \item {\tt sumE2} theorem, 42
6.1608 + \item {\tt SumE_fst} theorem, 115, 117, 129, 130
6.1609 + \item {\tt SumE_snd} theorem, 115, 117, 131
6.1610 + \item {\tt SumEL} theorem, 115
6.1611 + \item {\tt SumF} theorem, 115
6.1612 + \item {\tt SumFL} theorem, 115
6.1613 + \item {\tt SumI} theorem, 115, 125
6.1614 + \item {\tt SumIL} theorem, 115
6.1615 + \item {\tt SumIL2} theorem, 117
6.1616 + \item {\tt surj} constant, 44, 72
6.1617 + \item {\tt surj_def} theorem, 44, 72
6.1618 + \item {\tt surjective_pairing} theorem, 74
6.1619 + \item {\tt surjective_sum} theorem, 76
6.1620 + \item {\tt swap} theorem, 10, 64
6.1621 + \item {\tt swap_res_tac}, 15, 96
6.1622 + \item {\tt sym} theorem, 8, 63, 100
6.1623 + \item {\tt sym_elem} theorem, 113
6.1624 + \item {\tt sym_type} theorem, 113
6.1625 + \item {\tt symL} theorem, 101
6.1626
6.1627 \indexspace
6.1628
6.1629 - \item {\ptt T} constant, 111
6.1630 - \item {\ptt t} type, 110
6.1631 - \item {\ptt TC} theorem, 117
6.1632 - \item {\ptt TE} theorem, 117
6.1633 - \item {\ptt TEL} theorem, 117
6.1634 - \item {\ptt term} class, 4, 58, 60, 63, 98
6.1635 - \item {\ptt test_assume_tac}, \bold{120}
6.1636 - \item {\ptt TF} theorem, 117
6.1637 - \item {\ptt THE} symbol, 25, 27, 35, 99
6.1638 - \item {\ptt The} constant, 24, 27, 28, 99
6.1639 - \item {\ptt The} theorem, 101
6.1640 - \item {\ptt the_def} theorem, 29
6.1641 - \item {\ptt the_equality} theorem, 34, 35
6.1642 - \item {\ptt theI} theorem, 34, 35
6.1643 - \item {\ptt thinL} theorem, 101
6.1644 - \item {\ptt thinR} theorem, 101
6.1645 - \item {\ptt TI} theorem, 117
6.1646 - \item {\ptt times} class, 58
6.1647 - \item {\ptt tl} constant, 80
6.1648 - \item {\ptt tl_Cons} theorem, 81
6.1649 + \item {\tt T} constant, 110
6.1650 + \item {\tt t} type, 109
6.1651 + \item {\tt take} constant, 79
6.1652 + \item {\tt takeWhile} constant, 79
6.1653 + \item {\tt TC} theorem, 116
6.1654 + \item {\tt TE} theorem, 116
6.1655 + \item {\tt TEL} theorem, 116
6.1656 + \item {\tt term} class, 4, 59, 97
6.1657 + \item {\tt test_assume_tac}, \bold{118}
6.1658 + \item {\tt TF} theorem, 116
6.1659 + \item {\tt THE} symbol, 25, 27, 35, 98
6.1660 + \item {\tt The} constant, 24, 27, 28, 98
6.1661 + \item {\tt The} theorem, 100
6.1662 + \item {\tt the_def} theorem, 29
6.1663 + \item {\tt the_equality} theorem, 34, 35
6.1664 + \item {\tt theI} theorem, 34, 35
6.1665 + \item {\tt thinL} theorem, 100
6.1666 + \item {\tt thinR} theorem, 100
6.1667 + \item {\tt TI} theorem, 116
6.1668 + \item {\tt times} class, 59
6.1669 + \item {\tt tl} constant, 79
6.1670 \item tracing
6.1671 - \subitem of unification, 63
6.1672 - \item {\ptt trans} theorem, 8, 64, 101
6.1673 - \item {\ptt trans_elem} theorem, 114
6.1674 - \item {\ptt trans_red} theorem, 114
6.1675 - \item {\ptt trans_type} theorem, 114
6.1676 - \item {\ptt True} constant, 6, 59, 99
6.1677 - \item {\ptt True_def} theorem, 7, 62, 101
6.1678 - \item {\ptt True_or_False} theorem, 62, 63
6.1679 - \item {\ptt TrueI} theorem, 8, 64
6.1680 - \item {\ptt Trueprop} constant, 6, 59, 99
6.1681 - \item {\ptt TrueR} theorem, 102
6.1682 - \item {\ptt tt} constant, 111
6.1683 - \item {\ptt ttl} constant, 80
6.1684 - \item {\ptt ttl_Cons} theorem, 81
6.1685 - \item {\ptt ttl_Nil} theorem, 81
6.1686 - \item {\ptt Type} constant, 111
6.1687 - \item type definition, \bold{82}
6.1688 - \item {\ptt typechk_tac}, \bold{120}, 124, 127, 132
6.1689 + \subitem of unification, 60
6.1690 + \item {\tt trans} theorem, 8, 63, 100
6.1691 + \item {\tt trans_elem} theorem, 113
6.1692 + \item {\tt trans_red} theorem, 113
6.1693 + \item {\tt trans_tac}, 77
6.1694 + \item {\tt trans_type} theorem, 113
6.1695 + \item {\tt True} constant, 6, 58, 98
6.1696 + \item {\tt True_def} theorem, 7, 62, 100
6.1697 + \item {\tt True_or_False} theorem, 61
6.1698 + \item {\tt TrueI} theorem, 8, 63
6.1699 + \item {\tt Trueprop} constant, 6, 58, 98
6.1700 + \item {\tt TrueR} theorem, 101
6.1701 + \item {\tt tt} constant, 110
6.1702 + \item {\tt ttl} constant, 79
6.1703 + \item {\tt Type} constant, 110
6.1704 + \item type definition, \bold{78}
6.1705 + \item {\tt typechk_tac}, \bold{118}, 123, 126, 130, 131
6.1706
6.1707 \indexspace
6.1708
6.1709 - \item {\ptt UN} symbol, 25, 27, 66, 67, 69
6.1710 - \item {\ptt Un} symbol, 24, 66
6.1711 - \item {\ptt Un1} theorem, 72
6.1712 - \item {\ptt Un2} theorem, 72
6.1713 - \item {\ptt Un_absorb} theorem, 41, 73
6.1714 - \item {\ptt Un_assoc} theorem, 41, 73
6.1715 - \item {\ptt Un_commute} theorem, 41, 73
6.1716 - \item {\ptt Un_def} theorem, 29, 69
6.1717 - \item {\ptt UN_E} theorem, 33, 71
6.1718 - \item {\ptt UN_I} theorem, 33, 71
6.1719 - \item {\ptt Un_Int_distrib} theorem, 41, 73
6.1720 - \item {\ptt Un_Inter} theorem, 73
6.1721 - \item {\ptt Un_Inter_RepFun} theorem, 41
6.1722 - \item {\ptt Un_least} theorem, 35, 73
6.1723 - \item {\ptt Un_Union_image} theorem, 73
6.1724 - \item {\ptt Un_upper1} theorem, 35, 73
6.1725 - \item {\ptt Un_upper2} theorem, 35, 73
6.1726 - \item {\ptt UnCI} theorem, 34, 35, 71, 72
6.1727 - \item {\ptt UnE} theorem, 34, 71
6.1728 - \item {\ptt UnI1} theorem, 34, 35, 56, 71
6.1729 - \item {\ptt UnI2} theorem, 34, 35, 71
6.1730 + \item {\tt UN} symbol, 25, 27, 65, 66, 68
6.1731 + \item {\tt Un} symbol, 24, 65
6.1732 + \item {\tt Un1} theorem, 72
6.1733 + \item {\tt Un2} theorem, 72
6.1734 + \item {\tt Un_absorb} theorem, 40, 71
6.1735 + \item {\tt Un_assoc} theorem, 40, 71
6.1736 + \item {\tt Un_commute} theorem, 40, 71
6.1737 + \item {\tt Un_def} theorem, 29, 68
6.1738 + \item {\tt UN_E} theorem, 33, 70
6.1739 + \item {\tt UN_I} theorem, 33, 70
6.1740 + \item {\tt Un_Int_distrib} theorem, 40, 71
6.1741 + \item {\tt Un_Inter} theorem, 71
6.1742 + \item {\tt Un_Inter_RepFun} theorem, 40
6.1743 + \item {\tt Un_least} theorem, 35, 71
6.1744 + \item {\tt Un_Union_image} theorem, 71
6.1745 + \item {\tt Un_upper1} theorem, 35, 71
6.1746 + \item {\tt Un_upper2} theorem, 35, 71
6.1747 + \item {\tt UnCI} theorem, 34, 35, 70, 72
6.1748 + \item {\tt UnE} theorem, 34, 70
6.1749 + \item {\tt UnI1} theorem, 34, 35, 55, 70
6.1750 + \item {\tt UnI2} theorem, 34, 35, 70
6.1751 \item unification
6.1752 - \subitem incompleteness of, 63
6.1753 - \item {\ptt Unify.trace_types}, 63
6.1754 - \item {\ptt UNION} constant, 66
6.1755 - \item {\ptt Union} constant, 24, 66
6.1756 - \item {\ptt UNION1} constant, 66
6.1757 - \item {\ptt UNION1_def} theorem, 69
6.1758 - \item {\ptt UNION_def} theorem, 69
6.1759 - \item {\ptt Union_def} theorem, 69
6.1760 - \item {\ptt Union_iff} theorem, 29
6.1761 - \item {\ptt Union_least} theorem, 35, 73
6.1762 - \item {\ptt Union_Un_distrib} theorem, 41, 73
6.1763 - \item {\ptt Union_upper} theorem, 35, 73
6.1764 - \item {\ptt UnionE} theorem, 33, 54, 71
6.1765 - \item {\ptt UnionI} theorem, 33, 54, 71
6.1766 - \item {\ptt unit_eq} theorem, 76
6.1767 - \item {\ptt Univ} theory, 43
6.1768 - \item {\ptt Upair} constant, 23, 24, 28
6.1769 - \item {\ptt Upair_def} theorem, 29
6.1770 - \item {\ptt UpairE} theorem, 33
6.1771 - \item {\ptt UpairI1} theorem, 33
6.1772 - \item {\ptt UpairI2} theorem, 33
6.1773 + \subitem incompleteness of, 60
6.1774 + \item {\tt Unify.trace_types}, 60
6.1775 + \item {\tt UNION} constant, 65
6.1776 + \item {\tt Union} constant, 24, 65
6.1777 + \item {\tt UNION1} constant, 65
6.1778 + \item {\tt UNION1_def} theorem, 68
6.1779 + \item {\tt UNION_def} theorem, 68
6.1780 + \item {\tt Union_def} theorem, 68
6.1781 + \item {\tt Union_iff} theorem, 29
6.1782 + \item {\tt Union_least} theorem, 35, 71
6.1783 + \item {\tt Union_Un_distrib} theorem, 40, 71
6.1784 + \item {\tt Union_upper} theorem, 35, 71
6.1785 + \item {\tt UnionE} theorem, 33, 54, 70
6.1786 + \item {\tt UnionI} theorem, 33, 54, 70
6.1787 + \item {\tt unit_eq} theorem, 75
6.1788 + \item {\tt Univ} theory, 45
6.1789 + \item {\tt Upair} constant, 23, 24, 28
6.1790 + \item {\tt Upair_def} theorem, 29
6.1791 + \item {\tt UpairE} theorem, 33
6.1792 + \item {\tt UpairI1} theorem, 33
6.1793 + \item {\tt UpairI2} theorem, 33
6.1794
6.1795 \indexspace
6.1796
6.1797 - \item {\ptt vimage_def} theorem, 30
6.1798 - \item {\ptt vimageE} theorem, 38
6.1799 - \item {\ptt vimageI} theorem, 38
6.1800 + \item {\tt vimage_def} theorem, 30
6.1801 + \item {\tt vimageE} theorem, 37
6.1802 + \item {\tt vimageI} theorem, 37
6.1803
6.1804 \indexspace
6.1805
6.1806 - \item {\ptt when} constant, 111, 118, 126
6.1807 + \item {\tt when} constant, 110, 115, 124
6.1808
6.1809 \indexspace
6.1810
6.1811 - \item {\ptt xor_def} theorem, 42
6.1812 + \item {\tt xor_def} theorem, 41
6.1813
6.1814 \indexspace
6.1815
6.1816 - \item {\ptt zero_less_Suc} theorem, 79
6.1817 - \item {\ptt zero_ne_succ} theorem, 115, 116
6.1818 - \item {\ptt ZF} theory, 1, 22, 58
6.1819 - \item {\ptt ZF_cs}, \bold{22}
6.1820 - \item {\ptt ZF_ss}, \bold{22}
6.1821 + \item {\tt zero_ne_succ} theorem, 113, 114
6.1822 + \item {\tt ZF} theory, 1, 22, 57
6.1823 + \item {\tt ZF_cs}, \bold{22}
6.1824 + \item {\tt ZF_ss}, \bold{22}
6.1825
6.1826 \end{theindex}
7.1 --- a/doc-src/Logics/logics.rao Fri May 02 16:18:11 1997 +0200
7.2 +++ b/doc-src/Logics/logics.rao Fri May 02 16:18:49 1997 +0200
7.3 @@ -1,80 +1,80 @@
7.4 -% This file was generated by 'rail' from 'logics.rai'
7.5 +% This file was generated by '/usr/stud/berghofe/latex/rail/rail' from 'logics.rai'
7.6 \rail@i {1}{ typedef : 'typedef' ( () | '(' tname ')') type '=' set witness; type : typevarlist name ( () | '(' infix ')' ); tname : name; set : string; witness : () | '(' id ')'; }
7.7 \rail@o {1}{
7.8 \rail@begin{2}{typedef}
7.9 -\rail@term{typedef}
7.10 +\rail@term{typedef}[]
7.11 \rail@bar
7.12 \rail@nextbar{1}
7.13 -\rail@term{(}
7.14 -\rail@nont{tname}
7.15 -\rail@term{)}
7.16 +\rail@term{(}[]
7.17 +\rail@nont{tname}[]
7.18 +\rail@term{)}[]
7.19 \rail@endbar
7.20 -\rail@nont{type}
7.21 -\rail@term{=}
7.22 -\rail@nont{set}
7.23 -\rail@nont{witness}
7.24 +\rail@nont{type}[]
7.25 +\rail@term{=}[]
7.26 +\rail@nont{set}[]
7.27 +\rail@nont{witness}[]
7.28 \rail@end
7.29 \rail@begin{2}{type}
7.30 -\rail@nont{typevarlist}
7.31 -\rail@nont{name}
7.32 +\rail@nont{typevarlist}[]
7.33 +\rail@nont{name}[]
7.34 \rail@bar
7.35 \rail@nextbar{1}
7.36 -\rail@term{(}
7.37 -\rail@nont{infix}
7.38 -\rail@term{)}
7.39 +\rail@term{(}[]
7.40 +\rail@nont{infix}[]
7.41 +\rail@term{)}[]
7.42 \rail@endbar
7.43 \rail@end
7.44 \rail@begin{1}{tname}
7.45 -\rail@nont{name}
7.46 +\rail@nont{name}[]
7.47 \rail@end
7.48 \rail@begin{1}{set}
7.49 -\rail@nont{string}
7.50 +\rail@nont{string}[]
7.51 \rail@end
7.52 \rail@begin{2}{witness}
7.53 \rail@bar
7.54 \rail@nextbar{1}
7.55 -\rail@term{(}
7.56 -\rail@nont{id}
7.57 -\rail@term{)}
7.58 +\rail@term{(}[]
7.59 +\rail@nont{id}[]
7.60 +\rail@term{)}[]
7.61 \rail@endbar
7.62 \rail@end
7.63 }
7.64 \rail@i {2}{ typedecl : typevarlist id '=' (cons + '|') ; cons : name (typ *) ( () | mixfix ) ; typ : id | tid | ('(' typevarlist id ')') ; }
7.65 \rail@o {2}{
7.66 \rail@begin{2}{typedecl}
7.67 -\rail@nont{typevarlist}
7.68 -\rail@nont{id}
7.69 -\rail@term{=}
7.70 +\rail@nont{typevarlist}[]
7.71 +\rail@nont{id}[]
7.72 +\rail@term{=}[]
7.73 \rail@plus
7.74 -\rail@nont{cons}
7.75 +\rail@nont{cons}[]
7.76 \rail@nextplus{1}
7.77 -\rail@cterm{|}
7.78 +\rail@cterm{|}[]
7.79 \rail@endplus
7.80 \rail@end
7.81 \rail@begin{3}{cons}
7.82 -\rail@nont{name}
7.83 +\rail@nont{name}[]
7.84 \rail@bar
7.85 \rail@nextbar{1}
7.86 \rail@plus
7.87 -\rail@nont{typ}
7.88 +\rail@nont{typ}[]
7.89 \rail@nextplus{2}
7.90 \rail@endplus
7.91 \rail@endbar
7.92 \rail@bar
7.93 \rail@nextbar{1}
7.94 -\rail@nont{mixfix}
7.95 +\rail@nont{mixfix}[]
7.96 \rail@endbar
7.97 \rail@end
7.98 \rail@begin{3}{typ}
7.99 \rail@bar
7.100 -\rail@nont{id}
7.101 +\rail@nont{id}[]
7.102 \rail@nextbar{1}
7.103 -\rail@nont{tid}
7.104 +\rail@nont{tid}[]
7.105 \rail@nextbar{2}
7.106 -\rail@term{(}
7.107 -\rail@nont{typevarlist}
7.108 -\rail@nont{id}
7.109 -\rail@term{)}
7.110 +\rail@term{(}[]
7.111 +\rail@nont{typevarlist}[]
7.112 +\rail@nont{id}[]
7.113 +\rail@term{)}[]
7.114 \rail@endbar
7.115 \rail@end
7.116 }
8.1 --- a/doc-src/Logics/logics.tex Fri May 02 16:18:11 1997 +0200
8.2 +++ b/doc-src/Logics/logics.tex Fri May 02 16:18:49 1997 +0200
8.3 @@ -1,7 +1,9 @@
8.4 -\documentstyle[a4,12pt]{report}
8.5 +\documentclass[12pt]{report}
8.6 +\usepackage{a4,latexsym}
8.7 +
8.8 \makeatletter
8.9 \input{../rail.sty}
8.10 -\input{../proof209.sty}
8.11 +\input{../proof.sty}
8.12 \input{../iman.sty}
8.13 \input{../extra.sty}
8.14 \makeatother
9.1 --- a/doc-src/iman.sty Fri May 02 16:18:11 1997 +0200
9.2 +++ b/doc-src/iman.sty Fri May 02 16:18:49 1997 +0200
9.3 @@ -140,40 +140,14 @@
9.4 \newfont{\sltt}{cmsltt10} %% for output from terminal sessions
9.5 \newcommand\out{\ \sltt}
9.6
9.7 -% "itmath.sty" use cmr italic for letters in math mode and get the
9.8 -% usual letter spacing of text mode.
9.9 -%
9.10 -% Michael Lawley, April 1993
9.11 -% (lawley@cit.gu.edu.au)
9.12 -%
9.13 -% Derived from itma.sty (of unknown origin).
9.14 -%
9.15 -% MATHCODES
9.16 -%
9.17 % The mathcodes for the letters A, ..., Z, a, ..., z are changed to
9.18 % generate text italic rather than math italic by default. This makes
9.19 % multi-letter identifiers look better. The mathcode for character c
9.20 -% is set to "7000 (variable class) + "400 (text italic) + c.
9.21 +% is set to |"7000| (variable family) + |"400| (text italic) + |c|.
9.22 %
9.23 -% For NFSS the mathcode is "7000 (variable class) + (hex)\itfam + c
9.24 -% \itfam is probably equal to 7.
9.25 -%
9.26 -
9.27 -\ifx\undefined\hexnumber@
9.28 - \def\hexnumber@#1{\ifcase#1 \z@
9.29 - \or \@ne \or \tw@ \or \thr@@
9.30 - \or 4\or 5\or 6\or 7\or 8\or
9.31 - 9\or A\or B\or C\or D\or E\or F\fi}
9.32 -\fi
9.33 -
9.34 +\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
9.35 \def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
9.36 \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
9.37 \advance\count0 by1 \advance\count1 by1 \repeat}}
9.38 -
9.39 -\edef\@tempa{\hexnumber@\itfam}
9.40 -
9.41 -\@setmcodes{`A}{`Z}{"7\@tempa 41}
9.42 -\@setmcodes{`a}{`z}{"7\@tempa 61}
9.43 -
9.44 -\ifx\define@mathgroup\undefined\else
9.45 - \define@mathgroup\mv@normal{\itfam}{cmr}{m}{it}\fi
9.46 +\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}
9.47 +\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}
10.1 --- a/doc-src/sedindex Fri May 02 16:18:11 1997 +0200
10.2 +++ b/doc-src/sedindex Fri May 02 16:18:49 1997 +0200
10.3 @@ -5,18 +5,17 @@
10.4 # puts strings prefixed by * into \tt font
10.5 # terminator characters for strings are |!@{}
10.6 #
10.7 -# uses \ptt instead of \tt since that happens to explicit \tt's
10.8 # a space terminates the \tt part to allow \index{*NE theorem}, etc.
10.9 #
10.10 -# change *"X"Y"Z"W to "X"Y"Z"W@{\ptt "X"Y"Z"W}
10.11 -# change *"X"Y"Z to "X"Y"Z@{\ptt "X"Y"Z}
10.12 -# change *"X"Y to "X"Y@{\ptt "X"Y}
10.13 -# change *"X to "X@{\ptt "X}
10.14 -# change *IDENT to IDENT@{\ptt IDENT}
10.15 +# change *"X"Y"Z"W to "X"Y"Z"W@{\tt "X"Y"Z"W}
10.16 +# change *"X"Y"Z to "X"Y"Z@{\tt "X"Y"Z}
10.17 +# change *"X"Y to "X"Y@{\tt "X"Y}
10.18 +# change *"X to "X@{\tt "X}
10.19 +# change *IDENT to IDENT@{\tt IDENT}
10.20 # where IDENT is any string not containing | ! or @
10.21 # FOUR backslashes: to escape the shell AND sed
10.22 -sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\ptt \1}~g
10.23 -s~\*\(\".\".\".\)~\1@{\\\\ptt \1}~g
10.24 -s~\*\(\".\".\)~\1@{\\\\ptt \1}~g
10.25 -s~\*\(\".\)~\1@{\\\\ptt \1}~g
10.26 -s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\ptt \1}~g" $1.idx | makeindex -c -q -o $1.ind
10.27 +sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\tt \1}~g
10.28 +s~\*\(\".\".\".\)~\1@{\\\\tt \1}~g
10.29 +s~\*\(\".\".\)~\1@{\\\\tt \1}~g
10.30 +s~\*\(\".\)~\1@{\\\\tt \1}~g
10.31 +s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\tt \1}~g" $1.idx | makeindex -c -q -o $1.ind