Updated to LaTeX 2e
authorberghofe
Fri May 02 16:18:49 1997 +0200 (1997-05-02)
changeset 3096ccc2c92bb232
parent 3095 20251c80be78
child 3097 ae362c99a635
Updated to LaTeX 2e
doc-src/Intro/Makefile
doc-src/Intro/intro.ind
doc-src/Intro/intro.tex
doc-src/Logics/CTT.tex
doc-src/Logics/Makefile
doc-src/Logics/logics.ind
doc-src/Logics/logics.rao
doc-src/Logics/logics.tex
doc-src/iman.sty
doc-src/sedindex
     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 -%
    9.22 -% For NFSS the mathcode is "7000 (variable class) + (hex)\itfam + c
    9.23 -% \itfam is probably equal to 7.
    9.24 +% is set to |"7000| (variable family) + |"400| (text italic) + |c|.
    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