doc-src/Intro/intro.ind

   \indexspace
 
   \item {\ptt allI} theorem, 35
   \item arities
     \subitem declaring, 4, \bold{47}
-  \item {\ptt asm_simp_tac}, 56
+  \item {\ptt asm_simp_tac}, 57
   \item {\ptt assume_tac}, 28, 30, 35, 44
   \item assumptions
     \subitem deleting, 19
     \subitem discharge of, 7
     \subitem lifting over, 13
     \subitem of main goal, 39
     \subitem use of, 16, 27
   \item axioms
-    \subitem Peano, 51
+    \subitem Peano, 52
 
   \indexspace
 
   \item {\ptt ba}, 29
-  \item {\ptt back}, 55, 59
+  \item {\ptt back}, 55, 56, 59
   \item backtracking
-    \subitem Prolog style, 58
+    \subitem Prolog style, 59
   \item {\ptt bd}, 29
   \item {\ptt be}, 29
   \item {\ptt br}, 29
   \item {\ptt by}, 29
 
   \indexspace
 
-  \item {\ptt choplev}, 34, 35, 60
+  \item {\ptt choplev}, 34, 35, 61
   \item classes, 3
     \subitem built-in, \bold{24}
   \item classical reasoner, 37
   \item {\ptt conjunct1} theorem, 26
   \item constants, 1
     \subitem clashes with variables, 9
     \subitem declaring, \bold{46}
-    \subitem overloaded, 50
+    \subitem overloaded, 51
     \subitem polymorphic, 3
 
   \indexspace
 
   \item definitions, 5, \bold{46}

   \item examples
     \subitem of deriving rules, 39
     \subitem of induction, 54, 55
     \subitem of simplification, 56
     \subitem of tacticals, 35
-    \subitem of theories, 46--52, 57
+    \subitem of theories, 46, 48--53, 58
     \subitem propositional, 16, 29, 31
     \subitem with quantifiers, 17, 32, 33, 36
   \item {\ptt exE} theorem, 36
 
   \indexspace

   \item {\ptt goal}, 29, 39, 44
   \item {\ptt goalw}, 42--44
 
   \indexspace
 
-  \item {\ptt has_fewer_prems}, 60
+  \item {\ptt has_fewer_prems}, 61
   \item higher-order logic, 4
 
   \indexspace
 
   \item identifiers, 23
   \item {\ptt impI} theorem, 30, 42
   \item infixes, 49
-  \item instantiation, 53--57
+  \item instantiation, 54--57
   \item Isabelle
     \subitem object-logics supported, i
     \subitem overview, i
     \subitem release history, i
 

     \subitem syntax of, 21
   \item meta-equality, \bold{5}, 24
   \item meta-implication, \bold{5}, 6, 24
   \item meta-quantifiers, \bold{5}, 7, 24
   \item meta-rewriting, 41
-  \item mixfix declarations, 49, 50, 52
+  \item mixfix declarations, 49, 50, 53
   \item ML, i
   \item {\ptt ML} section, 45
   \item {\ptt mp} theorem, 26
 
   \indexspace
 
-  \item {\ptt Nat} theory, 52
+  \item {\ptt Nat} theory, 53
   \item {\ptt nat} type, 1, 3
   \item {\ptt not_def} theorem, 42
-  \item {\ptt notE} theorem, \bold{43}, 54
-  \item {\ptt notI} theorem, \bold{42}, 54
+  \item {\ptt notE} theorem, \bold{43}, 55
+  \item {\ptt notI} theorem, \bold{42}, 55
 
   \indexspace
 
   \item {\ptt o} type, 1, 4
   \item {\ptt ORELSE}, 35
-  \item overloading, \bold{4}, 50
+  \item overloading, \bold{4}, 51
 
   \indexspace
 
   \item parameters, \bold{7}, 32
     \subitem lifting over, 14
-  \item {\ptt Prolog} theory, 57
+  \item {\ptt Prolog} theory, 58
   \item Prolog interpreter, \bold{57}
   \item proof state, 15
   \item proofs
     \subitem commands for, 29
   \item {\ptt PROP} symbol, 25

 
   \indexspace
 
   \item {\ptt read_instantiate}, 28
   \item {\ptt refl} theorem, 28
-  \item {\ptt REPEAT}, 31, 36, 58, 60
-  \item {\ptt res_inst_tac}, 53, 56
+  \item {\ptt REPEAT}, 31, 36, 59, 60
+  \item {\ptt res_inst_tac}, 54, 56
   \item reserved words, 23
   \item resolution, 10, \bold{11}
     \subitem in backward proof, 15
-    \subitem with instantiation, 53
+    \subitem with instantiation, 54
   \item {\ptt resolve_tac}, 28, 30, 43, 55
   \item {\ptt result}, 29, 40, 44
   \item {\ptt rewrite_goals_tac}, 42
   \item {\ptt rewrite_rule}, 43
   \item {\ptt RL}, 27, 28

     \subitem quantifier, 7
 
   \indexspace
 
   \item search
-    \subitem depth-first, 59
+    \subitem depth-first, 60
   \item signatures, \bold{8}
-  \item {\ptt simp_tac}, 56
+  \item {\ptt simp_tac}, 57
   \item simplification, 56
   \item simplification sets, 56
   \item sort constraints, 24
   \item sorts, \bold{4}
   \item {\ptt spec} theorem, 26, 34, 35
   \item {\ptt standard}, 26
   \item substitution, \bold{7}
-  \item {\ptt Suc_inject}, 54
-  \item {\ptt Suc_neq_0}, 54
+  \item {\ptt Suc_inject}, 55
+  \item {\ptt Suc_neq_0}, 55
   \item syntax
     \subitem of types and terms, 24
 
   \indexspace
 

     \subitem syntax of, 1, \bold{24}
   \item theorems
     \subitem basic operations on, \bold{25}
     \subitem printing of, 25
   \item theories, \bold{8}
-    \subitem defining, 44--53
+    \subitem defining, 44--54
   \item {\ptt thm} ML type, 25
   \item {\ptt topthm}, 40
   \item {\ptt Trueprop} constant, 6, 24
   \item type constraints, 24
   \item type constructors, 1
   \item type identifiers, 23
-  \item type synonyms, \bold{48}
+  \item type synonyms, \bold{49}
   \item types
     \subitem declaring, \bold{47}
     \subitem function, 1
     \subitem higher, \bold{5}
     \subitem polymorphic, \bold{3}