1.1 --- a/doc-src/Intro/intro.bbl	Thu Apr 17 18:16:12 1997 +0200
     1.2 +++ b/doc-src/Intro/intro.bbl	Thu Apr 17 18:17:23 1997 +0200
     1.3 @@ -85,7 +85,7 @@
     1.4  F.~J. Pelletier.
     1.5  \newblock Seventy-five problems for testing automatic theorem provers.
     1.6  \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
     1.7 -\newblock Errata, JAR 4 (1988), 235--236.
     1.8 +\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
     1.9  
    1.10  \bibitem{reeves90}
    1.11  Steve Reeves and Michael Clarke.

     2.1 --- a/doc-src/Intro/intro.ind	Thu Apr 17 18:16:12 1997 +0200
     2.2 +++ b/doc-src/Intro/intro.ind	Thu Apr 17 18:17:23 1997 +0200
     2.3 @@ -1,115 +1,115 @@
     2.4  \begin{theindex}
     2.5  
     2.6 -  \item {\ptt !!} symbol, 25
     2.7 -    \subitem in main goal, 46
     2.8 -  \item {\tt\%} symbol, 25
     2.9 -  \item {\ptt ::} symbol, 25
    2.10 -  \item {\ptt ==} symbol, 25
    2.11 -  \item {\ptt ==>} symbol, 25
    2.12 -  \item {\ptt =>} symbol, 25
    2.13 -  \item {\ptt =?=} symbol, 25
    2.14 -  \item {\ptt [} symbol, 25
    2.15 -  \item {\ptt [|} symbol, 25
    2.16 -  \item {\ptt ]} symbol, 25
    2.17 -  \item {\tt\ttlbrace} symbol, 25
    2.18 -  \item {\tt\ttrbrace} symbol, 25
    2.19 -  \item {\ptt |]} symbol, 25
    2.20 +  \item {\ptt !!} symbol, 24
    2.21 +    \subitem in main goal, 44
    2.22 +  \item {\tt\%} symbol, 24
    2.23 +  \item {\ptt ::} symbol, 24
    2.24 +  \item {\ptt ==} symbol, 24
    2.25 +  \item {\ptt ==>} symbol, 24
    2.26 +  \item {\ptt =>} symbol, 24
    2.27 +  \item {\ptt =?=} symbol, 24
    2.28 +  \item {\ptt [} symbol, 24
    2.29 +  \item {\ptt [|} symbol, 24
    2.30 +  \item {\ptt ]} symbol, 24
    2.31 +  \item {\tt\ttlbrace} symbol, 24
    2.32 +  \item {\tt\ttrbrace} symbol, 24
    2.33 +  \item {\ptt |]} symbol, 24
    2.34  
    2.35    \indexspace
    2.36  
    2.37 -  \item {\ptt allI} theorem, 37
    2.38 +  \item {\ptt allI} theorem, 35
    2.39    \item arities
    2.40 -    \subitem declaring, 4, \bold{49}
    2.41 -  \item {\ptt asm_simp_tac}, 60
    2.42 -  \item {\ptt assume_tac}, 29, 31, 37, 47
    2.43 +    \subitem declaring, 4, \bold{47}
    2.44 +  \item {\ptt asm_simp_tac}, 57
    2.45 +  \item {\ptt assume_tac}, 28, 30, 35, 44
    2.46    \item assumptions
    2.47 -    \subitem deleting, 20
    2.48 +    \subitem deleting, 19
    2.49      \subitem discharge of, 7
    2.50 -    \subitem lifting over, 14
    2.51 -    \subitem of main goal, 41
    2.52 -    \subitem use of, 16, 28
    2.53 +    \subitem lifting over, 13
    2.54 +    \subitem of main goal, 39
    2.55 +    \subitem use of, 16, 27
    2.56    \item axioms
    2.57 -    \subitem Peano, 54
    2.58 +    \subitem Peano, 52
    2.59  
    2.60    \indexspace
    2.61  
    2.62 -  \item {\ptt ba}, 30
    2.63 -  \item {\ptt back}, 59, 62
    2.64 +  \item {\ptt ba}, 29
    2.65 +  \item {\ptt back}, 55, 56, 59
    2.66    \item backtracking
    2.67 -    \subitem Prolog style, 62
    2.68 -  \item {\ptt bd}, 30
    2.69 -  \item {\ptt be}, 30
    2.70 -  \item {\ptt br}, 30
    2.71 -  \item {\ptt by}, 30
    2.72 +    \subitem Prolog style, 59
    2.73 +  \item {\ptt bd}, 29
    2.74 +  \item {\ptt be}, 29
    2.75 +  \item {\ptt br}, 29
    2.76 +  \item {\ptt by}, 29
    2.77  
    2.78    \indexspace
    2.79  
    2.80 -  \item {\ptt choplev}, 36, 37, 64
    2.81 +  \item {\ptt choplev}, 34, 35, 61
    2.82    \item classes, 3
    2.83 -    \subitem built-in, \bold{25}
    2.84 -  \item classical reasoner, 39
    2.85 -  \item {\ptt conjunct1} theorem, 27
    2.86 +    \subitem built-in, \bold{24}
    2.87 +  \item classical reasoner, 37
    2.88 +  \item {\ptt conjunct1} theorem, 26
    2.89    \item constants, 1
    2.90      \subitem clashes with variables, 9
    2.91 -    \subitem declaring, \bold{48}
    2.92 -    \subitem overloaded, 53
    2.93 +    \subitem declaring, \bold{46}
    2.94 +    \subitem overloaded, 51
    2.95      \subitem polymorphic, 3
    2.96  
    2.97    \indexspace
    2.98  
    2.99 -  \item definitions, 6, \bold{48}
   2.100 -    \subitem and derived rules, 43--46
   2.101 -  \item {\ptt DEPTH_FIRST}, 64
   2.102 -  \item destruct-resolution, 22, 30
   2.103 -  \item {\ptt disjE} theorem, 31
   2.104 -  \item {\ptt dres_inst_tac}, 57
   2.105 -  \item {\ptt dresolve_tac}, 30, 32, 38
   2.106 +  \item definitions, 5, \bold{46}
   2.107 +    \subitem and derived rules, 41--44
   2.108 +  \item {\ptt DEPTH_FIRST}, 60
   2.109 +  \item destruct-resolution, 21, 29
   2.110 +  \item {\ptt disjE} theorem, 30
   2.111 +  \item {\ptt dres_inst_tac}, 54
   2.112 +  \item {\ptt dresolve_tac}, 29, 31, 36
   2.113  
   2.114    \indexspace
   2.115  
   2.116 -  \item eigenvariables, \see{parameters}{8}
   2.117 -  \item elim-resolution, \bold{20}, 30
   2.118 +  \item eigenvariables, \see{parameters}{7}
   2.119 +  \item elim-resolution, \bold{19}, 28
   2.120    \item equality
   2.121      \subitem polymorphic, 3
   2.122 -  \item {\ptt eres_inst_tac}, 57
   2.123 -  \item {\ptt eresolve_tac}, 30, 32, 38, 47
   2.124 +  \item {\ptt eres_inst_tac}, 54
   2.125 +  \item {\ptt eresolve_tac}, 28, 31, 36, 44
   2.126    \item examples
   2.127 -    \subitem of deriving rules, 41
   2.128 -    \subitem of induction, 57, 58
   2.129 -    \subitem of simplification, 59
   2.130 -    \subitem of tacticals, 37
   2.131 -    \subitem of theories, 48, 50--55, 61
   2.132 -    \subitem propositional, 17, 31, 32
   2.133 -    \subitem with quantifiers, 18, 33, 35, 37
   2.134 -  \item {\ptt exE} theorem, 38
   2.135 +    \subitem of deriving rules, 39
   2.136 +    \subitem of induction, 54, 55
   2.137 +    \subitem of simplification, 56
   2.138 +    \subitem of tacticals, 35
   2.139 +    \subitem of theories, 46, 48--53, 58
   2.140 +    \subitem propositional, 16, 29, 31
   2.141 +    \subitem with quantifiers, 17, 32, 33, 36
   2.142 +  \item {\ptt exE} theorem, 36
   2.143  
   2.144    \indexspace
   2.145  
   2.146 -  \item {\ptt FalseE} theorem, 45
   2.147 -  \item {\ptt fast_tac}, 39
   2.148 +  \item {\ptt FalseE} theorem, 43
   2.149 +  \item {\ptt fast_tac}, 37
   2.150    \item first-order logic, 1
   2.151 -  \item flex-flex constraints, 6, 25, \bold{28}
   2.152 -  \item {\ptt flexflex_rule}, 28
   2.153 -  \item forward proof, 21, 24--30
   2.154 +  \item flex-flex constraints, 5, 24, \bold{27}
   2.155 +  \item {\ptt flexflex_rule}, 27
   2.156 +  \item forward proof, 20, 23--29
   2.157    \item {\ptt fun} type, 1, 4
   2.158 -  \item function applications, 1, 8
   2.159 +  \item function applications, 1, 7
   2.160  
   2.161    \indexspace
   2.162  
   2.163 -  \item {\ptt goal}, 30, 41, 46
   2.164 -  \item {\ptt goalw}, 44--46
   2.165 +  \item {\ptt goal}, 29, 39, 44
   2.166 +  \item {\ptt goalw}, 42--44
   2.167  
   2.168    \indexspace
   2.169  
   2.170 -  \item {\ptt has_fewer_prems}, 64
   2.171 +  \item {\ptt has_fewer_prems}, 61
   2.172    \item higher-order logic, 4
   2.173  
   2.174    \indexspace
   2.175  
   2.176 -  \item identifiers, 24
   2.177 -  \item {\ptt impI} theorem, 31, 44
   2.178 -  \item infixes, 52
   2.179 -  \item instantiation, 57--60
   2.180 +  \item identifiers, 23
   2.181 +  \item {\ptt impI} theorem, 30, 42
   2.182 +  \item infixes, 49
   2.183 +  \item instantiation, 54--57
   2.184    \item Isabelle
   2.185      \subitem object-logics supported, i
   2.186      \subitem overview, i
   2.187 @@ -117,149 +117,149 @@
   2.188  
   2.189    \indexspace
   2.190  
   2.191 -  \item $\lambda$-abstractions, 1, 8, 25
   2.192 +  \item $\lambda$-abstractions, 1, 7, 24
   2.193    \item $\lambda$-calculus, 1
   2.194    \item LCF, i
   2.195 -  \item LCF system, 15, 26
   2.196 -  \item level of a proof, 31
   2.197 -  \item lifting, \bold{14}
   2.198 -  \item {\ptt logic} class, 3, 6, 25
   2.199 +  \item LCF system, 15, 25
   2.200 +  \item level of a proof, 29
   2.201 +  \item lifting, \bold{13}
   2.202 +  \item {\ptt logic} class, 3, 6, 24
   2.203  
   2.204    \indexspace
   2.205  
   2.206 -  \item major premise, \bold{21}
   2.207 -  \item {\ptt Match} exception, 42
   2.208 +  \item major premise, \bold{20}
   2.209 +  \item {\ptt Match} exception, 40
   2.210    \item meta-assumptions
   2.211 -    \subitem syntax of, 22
   2.212 -  \item meta-equality, \bold{5}, 25
   2.213 -  \item meta-implication, \bold{5}, 7, 25
   2.214 -  \item meta-quantifiers, \bold{5}, 8, 25
   2.215 -  \item meta-rewriting, 43
   2.216 -  \item mixfix declarations, 52, 53, 56
   2.217 +    \subitem syntax of, 21
   2.218 +  \item meta-equality, \bold{5}, 24
   2.219 +  \item meta-implication, \bold{5}, 6, 24
   2.220 +  \item meta-quantifiers, \bold{5}, 7, 24
   2.221 +  \item meta-rewriting, 41
   2.222 +  \item mixfix declarations, 49, 50, 53
   2.223    \item ML, i
   2.224 -  \item {\ptt ML} section, 47
   2.225 -  \item {\ptt mp} theorem, 27
   2.226 +  \item {\ptt ML} section, 45
   2.227 +  \item {\ptt mp} theorem, 26
   2.228  
   2.229    \indexspace
   2.230  
   2.231 -  \item {\ptt Nat} theory, 55
   2.232 +  \item {\ptt Nat} theory, 53
   2.233    \item {\ptt nat} type, 1, 3
   2.234 -  \item {\ptt not_def} theorem, 44
   2.235 -  \item {\ptt notE} theorem, \bold{45}, 58
   2.236 -  \item {\ptt notI} theorem, \bold{44}, 58
   2.237 +  \item {\ptt not_def} theorem, 42
   2.238 +  \item {\ptt notE} theorem, \bold{43}, 55
   2.239 +  \item {\ptt notI} theorem, \bold{42}, 55
   2.240  
   2.241    \indexspace
   2.242  
   2.243    \item {\ptt o} type, 1, 4
   2.244 -  \item {\ptt ORELSE}, 37
   2.245 -  \item overloading, \bold{4}, 53
   2.246 +  \item {\ptt ORELSE}, 35
   2.247 +  \item overloading, \bold{4}, 51
   2.248  
   2.249    \indexspace
   2.250  
   2.251 -  \item parameters, \bold{8}, 33
   2.252 -    \subitem lifting over, 15
   2.253 -  \item {\ptt Prolog} theory, 61
   2.254 -  \item Prolog interpreter, \bold{60}
   2.255 -  \item proof state, 16
   2.256 +  \item parameters, \bold{7}, 32
   2.257 +    \subitem lifting over, 14
   2.258 +  \item {\ptt Prolog} theory, 58
   2.259 +  \item Prolog interpreter, \bold{57}
   2.260 +  \item proof state, 15
   2.261    \item proofs
   2.262 -    \subitem commands for, 30
   2.263 -  \item {\ptt PROP} symbol, 26
   2.264 -  \item {\ptt prop} type, 6, 25, 26
   2.265 -  \item {\ptt prth}, 27
   2.266 -  \item {\ptt prthq}, 27, 28
   2.267 -  \item {\ptt prths}, 27
   2.268 -  \item {\ptt Pure} theory, 47
   2.269 +    \subitem commands for, 29
   2.270 +  \item {\ptt PROP} symbol, 25
   2.271 +  \item {\ptt prop} type, 6, 24
   2.272 +  \item {\ptt prth}, 26
   2.273 +  \item {\ptt prthq}, 26, 27
   2.274 +  \item {\ptt prths}, 26
   2.275 +  \item {\ptt Pure} theory, 45
   2.276  
   2.277    \indexspace
   2.278  
   2.279 -  \item quantifiers, 5, 8, 33
   2.280 +  \item quantifiers, 5, 7, 32
   2.281  
   2.282    \indexspace
   2.283  
   2.284 -  \item {\ptt read_instantiate}, 29
   2.285 -  \item {\ptt refl} theorem, 29
   2.286 -  \item {\ptt REPEAT}, 33, 37, 62, 64
   2.287 -  \item {\ptt res_inst_tac}, 57, 60
   2.288 -  \item reserved words, 24
   2.289 -  \item resolution, 10, \bold{12}
   2.290 +  \item {\ptt read_instantiate}, 28
   2.291 +  \item {\ptt refl} theorem, 28
   2.292 +  \item {\ptt REPEAT}, 31, 36, 59, 60
   2.293 +  \item {\ptt res_inst_tac}, 54, 56
   2.294 +  \item reserved words, 23
   2.295 +  \item resolution, 10, \bold{11}
   2.296      \subitem in backward proof, 15
   2.297 -    \subitem with instantiation, 57
   2.298 -  \item {\ptt resolve_tac}, 30, 31, 46, 58
   2.299 -  \item {\ptt result}, 30, 42, 46
   2.300 -  \item {\ptt rewrite_goals_tac}, 44
   2.301 -  \item {\ptt rewrite_rule}, 45, 46
   2.302 -  \item {\ptt RL}, 29
   2.303 -  \item {\ptt RLN}, 29
   2.304 -  \item {\ptt RS}, 27, 29, 46
   2.305 -  \item {\ptt RSN}, 27, 29
   2.306 +    \subitem with instantiation, 54
   2.307 +  \item {\ptt resolve_tac}, 28, 30, 43, 55
   2.308 +  \item {\ptt result}, 29, 40, 44
   2.309 +  \item {\ptt rewrite_goals_tac}, 42
   2.310 +  \item {\ptt rewrite_rule}, 43
   2.311 +  \item {\ptt RL}, 27, 28
   2.312 +  \item {\ptt RLN}, 27
   2.313 +  \item {\ptt RS}, 26, 27, 44
   2.314 +  \item {\ptt RSN}, 26, 27
   2.315    \item rules
   2.316 -    \subitem declaring, 48
   2.317 -    \subitem derived, 13, \bold{22}, 41, 43
   2.318 -    \subitem destruction, 21
   2.319 -    \subitem elimination, 21
   2.320 +    \subitem declaring, 46
   2.321 +    \subitem derived, 12, \bold{21}, 39, 41
   2.322 +    \subitem destruction, 20
   2.323 +    \subitem elimination, 20
   2.324      \subitem propositional, 6
   2.325 -    \subitem quantifier, 8
   2.326 +    \subitem quantifier, 7
   2.327  
   2.328    \indexspace
   2.329  
   2.330    \item search
   2.331 -    \subitem depth-first, 63
   2.332 -  \item signatures, \bold{9}
   2.333 -  \item {\ptt simp_tac}, 60
   2.334 -  \item simplification, 59
   2.335 -  \item simplification sets, 59
   2.336 -  \item sort constraints, 25
   2.337 -  \item sorts, \bold{5}
   2.338 -  \item {\ptt spec} theorem, 28, 36, 37
   2.339 -  \item {\ptt standard}, 27
   2.340 -  \item substitution, \bold{8}
   2.341 -  \item {\ptt Suc_inject}, 58
   2.342 -  \item {\ptt Suc_neq_0}, 58
   2.343 +    \subitem depth-first, 60
   2.344 +  \item signatures, \bold{8}
   2.345 +  \item {\ptt simp_tac}, 57
   2.346 +  \item simplification, 56
   2.347 +  \item simplification sets, 56
   2.348 +  \item sort constraints, 24
   2.349 +  \item sorts, \bold{4}
   2.350 +  \item {\ptt spec} theorem, 26, 34, 35
   2.351 +  \item {\ptt standard}, 26
   2.352 +  \item substitution, \bold{7}
   2.353 +  \item {\ptt Suc_inject}, 55
   2.354 +  \item {\ptt Suc_neq_0}, 55
   2.355    \item syntax
   2.356 -    \subitem of types and terms, 25
   2.357 +    \subitem of types and terms, 24
   2.358  
   2.359    \indexspace
   2.360  
   2.361 -  \item tacticals, \bold{19}, 37
   2.362 -  \item tactics, \bold{19}
   2.363 -    \subitem assumption, 29
   2.364 -    \subitem resolution, 30
   2.365 +  \item tacticals, \bold{18}, 35
   2.366 +  \item tactics, \bold{18}
   2.367 +    \subitem assumption, 28
   2.368 +    \subitem resolution, 28
   2.369    \item {\ptt term} class, 3
   2.370    \item terms
   2.371 -    \subitem syntax of, 1, \bold{25}
   2.372 +    \subitem syntax of, 1, \bold{24}
   2.373    \item theorems
   2.374 -    \subitem basic operations on, \bold{26}
   2.375 -    \subitem printing of, 27
   2.376 -  \item theories, \bold{9}
   2.377 -    \subitem defining, 47--57
   2.378 -  \item {\ptt thm} ML type, 26
   2.379 -  \item {\ptt topthm}, 42
   2.380 -  \item {\ptt Trueprop} constant, 6, 7, 25
   2.381 -  \item type constraints, 25
   2.382 +    \subitem basic operations on, \bold{25}
   2.383 +    \subitem printing of, 25
   2.384 +  \item theories, \bold{8}
   2.385 +    \subitem defining, 44--54
   2.386 +  \item {\ptt thm} ML type, 25
   2.387 +  \item {\ptt topthm}, 40
   2.388 +  \item {\ptt Trueprop} constant, 6, 24
   2.389 +  \item type constraints, 24
   2.390    \item type constructors, 1
   2.391 -  \item type identifiers, 24
   2.392 -  \item type synonyms, \bold{51}
   2.393 +  \item type identifiers, 23
   2.394 +  \item type synonyms, \bold{49}
   2.395    \item types
   2.396 -    \subitem declaring, \bold{49}
   2.397 +    \subitem declaring, \bold{47}
   2.398      \subitem function, 1
   2.399      \subitem higher, \bold{5}
   2.400      \subitem polymorphic, \bold{3}
   2.401      \subitem simple, \bold{1}
   2.402 -    \subitem syntax of, 1, \bold{25}
   2.403 +    \subitem syntax of, 1, \bold{24}
   2.404  
   2.405    \indexspace
   2.406  
   2.407 -  \item {\ptt undo}, 30
   2.408 +  \item {\ptt undo}, 29
   2.409    \item unification
   2.410 -    \subitem higher-order, \bold{11}, 58
   2.411 +    \subitem higher-order, \bold{10}, 55
   2.412      \subitem incompleteness of, 11
   2.413 -  \item unknowns, 10, 24, 33
   2.414 -    \subitem function, \bold{11}, 28, 33
   2.415 -  \item {\ptt use_thy}, \bold{47}
   2.416 +  \item unknowns, 9, 23, 32
   2.417 +    \subitem function, \bold{11}, 27, 32
   2.418 +  \item {\ptt use_thy}, \bold{45}
   2.419  
   2.420    \indexspace
   2.421  
   2.422    \item variables
   2.423 -    \subitem bound, 8
   2.424 +    \subitem bound, 7
   2.425  
   2.426  \end{theindex}