doc-src/Intro/intro.ind

 
   \item {\tt allI} theorem, 37
   \item arities
     \subitem declaring, 4, \bold{49}
   \item {\tt asm_simp_tac}, 60
-  \item {\tt assume_tac}, 29, 31, 37, 47
+  \item {\tt assume_tac}, 30, 32, 37, 47
   \item assumptions
     \subitem deleting, 20
     \subitem discharge of, 7
     \subitem lifting over, 14
     \subitem of main goal, 41

   \item axioms
     \subitem Peano, 54
 
   \indexspace
 
-  \item {\tt ba}, 30
+  \item {\tt ba}, 31
   \item {\tt back}, 59, 62
   \item backtracking
     \subitem Prolog style, 62
-  \item {\tt bd}, 30
-  \item {\tt be}, 30
-  \item {\tt br}, 30
+  \item {\tt bd}, 31
+  \item {\tt be}, 31
+  \item {\tt br}, 31
   \item {\tt by}, 30
 
   \indexspace
 
-  \item {\tt choplev}, 36, 37, 64
+  \item {\tt choplev}, 37, 64
   \item classes, 3
     \subitem built-in, \bold{25}
   \item classical reasoner, 39
-  \item {\tt conjunct1} theorem, 27
-  \item constants, 1
+  \item {\tt conjunct1} theorem, 28
+  \item constants, 3
     \subitem clashes with variables, 9
     \subitem declaring, \bold{48}
     \subitem overloaded, 53
     \subitem polymorphic, 3
+  \item {\tt CPure} theory, 47
 
   \indexspace
 
   \item definitions, 6, \bold{48}
     \subitem and derived rules, 43--46
   \item {\tt DEPTH_FIRST}, 64
   \item destruct-resolution, 22, 30
   \item {\tt disjE} theorem, 31
   \item {\tt dres_inst_tac}, 57
-  \item {\tt dresolve_tac}, 30, 32, 38
+  \item {\tt dresolve_tac}, 30, 32, 33, 38
 
   \indexspace
 
   \item eigenvariables, \see{parameters}{8}
   \item elim-resolution, \bold{20}, 30
   \item equality
     \subitem polymorphic, 3
   \item {\tt eres_inst_tac}, 57
-  \item {\tt eresolve_tac}, 30, 32, 38, 47
+  \item {\tt eresolve_tac}, 30, 32, 33, 39, 47
   \item examples
     \subitem of deriving rules, 41
     \subitem of induction, 57, 58
     \subitem of simplification, 59
     \subitem of tacticals, 37
     \subitem of theories, 48, 50--55, 61
     \subitem propositional, 17, 31, 32
-    \subitem with quantifiers, 18, 33, 35, 37
+    \subitem with quantifiers, 18, 34, 35, 38
   \item {\tt exE} theorem, 38
 
   \indexspace
 
   \item {\tt FalseE} theorem, 45
   \item {\tt fast_tac}, 39
   \item first-order logic, 1
   \item flex-flex constraints, 6, 25, \bold{28}
-  \item {\tt flexflex_rule}, 28
+  \item {\tt flexflex_rule}, 29
   \item forward proof, 21, 24--30
   \item {\tt fun} type, 1, 4
   \item function applications, 1, 8
 
   \indexspace

   \indexspace
 
   \item $\lambda$-abstractions, 1, 8, 25
   \item $\lambda$-calculus, 1
   \item LCF, i
-  \item LCF system, 15, 26
+  \item LCF system, 15, 27
   \item level of a proof, 31
   \item lifting, \bold{14}
   \item {\tt logic} class, 3, 6, 25
 
   \indexspace

   \item meta-quantifiers, \bold{5}, 8, 25
   \item meta-rewriting, 43
   \item mixfix declarations, 52, 53, 56
   \item ML, i
   \item {\tt ML} section, 47
-  \item {\tt mp} theorem, 27
+  \item {\tt mp} theorem, 27, 28
 
   \indexspace
 
   \item {\tt Nat} theory, 55
-  \item {\tt nat} type, 1, 3
+  \item {\tt nat} type, 3
   \item {\tt not_def} theorem, 44
-  \item {\tt notE} theorem, \bold{45}, 58
-  \item {\tt notI} theorem, \bold{44}, 58
-
-  \indexspace
-
-  \item {\tt o} type, 1, 4
-  \item {\tt ORELSE}, 37
+  \item {\tt notE} theorem, \bold{45}, 57
+  \item {\tt notI} theorem, \bold{44}, 57
+
+  \indexspace
+
+  \item {\tt o} type, 3, 4
+  \item {\tt ORELSE}, 38
   \item overloading, \bold{4}, 53
 
   \indexspace
 
-  \item parameters, \bold{8}, 33
+  \item parameters, \bold{8}, 34
     \subitem lifting over, 15
   \item {\tt Prolog} theory, 61
   \item Prolog interpreter, \bold{60}
   \item proof state, 16
   \item proofs
     \subitem commands for, 30
   \item {\tt PROP} symbol, 26
   \item {\tt prop} type, 6, 25, 26
   \item {\tt prth}, 27
-  \item {\tt prthq}, 27, 28
+  \item {\tt prthq}, 27, 29
   \item {\tt prths}, 27
   \item {\tt Pure} theory, 47
 
   \indexspace
 
-  \item quantifiers, 5, 8, 33
+  \item {\tt qed}, 31, 42, 46
+  \item quantifiers, 5, 8, 34
 
   \indexspace
 
   \item {\tt read_instantiate}, 29
   \item {\tt refl} theorem, 29
-  \item {\tt REPEAT}, 33, 37, 62, 64
-  \item {\tt res_inst_tac}, 57, 60
+  \item {\tt REPEAT}, 33, 38, 62, 64
+  \item {\tt res_inst_tac}, 57, 59
   \item reserved words, 24
   \item resolution, 10, \bold{12}
     \subitem in backward proof, 15
     \subitem with instantiation, 57
   \item {\tt resolve_tac}, 30, 31, 46, 58
-  \item {\tt result}, 30, 42, 46
+  \item {\tt result}, 31
   \item {\tt rewrite_goals_tac}, 44
   \item {\tt rewrite_rule}, 45, 46
   \item {\tt RL}, 29
   \item {\tt RLN}, 29
   \item {\tt RS}, 27, 29, 46

 
   \indexspace
 
   \item tacticals, \bold{19}, 37
   \item tactics, \bold{19}
-    \subitem assumption, 29
+    \subitem assumption, 30
     \subitem resolution, 30
   \item {\tt term} class, 3
   \item terms
     \subitem syntax of, 1, \bold{25}
   \item theorems
-    \subitem basic operations on, \bold{26}
+    \subitem basic operations on, \bold{27}
     \subitem printing of, 27
   \item theories, \bold{9}
-    \subitem defining, 47--57
-  \item {\tt thm} ML type, 26
+    \subitem defining, 47--56
+  \item {\tt thm} ML type, 27
   \item {\tt topthm}, 42
   \item {\tt Trueprop} constant, 6, 7, 25
   \item type constraints, 25
   \item type constructors, 1
   \item type identifiers, 24

 
   \item {\tt undo}, 30
   \item unification
     \subitem higher-order, \bold{11}, 58
     \subitem incompleteness of, 11
-  \item unknowns, 10, 24, 33
-    \subitem function, \bold{11}, 28, 33
-  \item {\tt use_thy}, \bold{47}
+  \item unknowns, 10, 24, 34
+    \subitem function, \bold{11}, 28, 34
+  \item {\tt use_thy}, \bold{47, 48}
 
   \indexspace
 
   \item variables
     \subitem bound, 8