diff -r 858da18069d7 -r 602354039306 doc-src/Intro/intro.ind
--- a/doc-src/Intro/intro.ind	Tue Jul 28 16:30:56 1998 +0200
+++ b/doc-src/Intro/intro.ind	Tue Jul 28 16:33:43 1998 +0200
@@ -1,7 +1,6 @@
 \begin{theindex}
 
   \item {\tt !!} symbol, 26
-    \subitem in main goal, 46
   \item {\tt\%} symbol, 25
   \item {\tt ::} symbol, 25
   \item {\tt ==} symbol, 26
@@ -19,9 +18,9 @@
 
   \item {\tt allI} theorem, 38
   \item arities
-    \subitem declaring, 4, \bold{49}
-  \item {\tt Asm_simp_tac}, 60
-  \item {\tt assume_tac}, 30, 32, 38, 47
+    \subitem declaring, 4, \bold{48}
+  \item {\tt Asm_simp_tac}, 59
+  \item {\tt assume_tac}, 30, 32, 38
   \item assumptions
     \subitem deleting, 20
     \subitem discharge of, 7
@@ -29,14 +28,14 @@
     \subitem of main goal, 41
     \subitem use of, 16, 28
   \item axioms
-    \subitem Peano, 55
+    \subitem Peano, 54
 
   \indexspace
 
   \item {\tt ba}, 31
-  \item {\tt back}, 59, 63
+  \item {\tt back}, 58, 62
   \item backtracking
-    \subitem Prolog style, 62
+    \subitem Prolog style, 61
   \item {\tt bd}, 31
   \item {\tt be}, 31
   \item {\tt Blast_tac}, 39, 40
@@ -45,26 +44,26 @@
 
   \indexspace
 
-  \item {\tt choplev}, 37, 38, 65
+  \item {\tt choplev}, 37, 38, 64
   \item classes, 3
     \subitem built-in, \bold{25}
   \item classical reasoner, 39
   \item {\tt conjunct1} theorem, 28
   \item constants, 3
     \subitem clashes with variables, 9
-    \subitem declaring, \bold{48}
-    \subitem overloaded, 54
+    \subitem declaring, \bold{47}
+    \subitem overloaded, 53
     \subitem polymorphic, 3
-  \item {\tt CPure} theory, 47
+  \item {\tt CPure} theory, 46
 
   \indexspace
 
-  \item definitions, 6, \bold{48}
-    \subitem and derived rules, 43--46
-  \item {\tt DEPTH_FIRST}, 64
+  \item definitions, 6, \bold{47}
+    \subitem and derived rules, 43--45
+  \item {\tt DEPTH_FIRST}, 63
   \item destruct-resolution, 22, 30
   \item {\tt disjE} theorem, 31
-  \item {\tt dres_inst_tac}, 57
+  \item {\tt dres_inst_tac}, 56
   \item {\tt dresolve_tac}, 30, 33, 39
 
   \indexspace
@@ -73,14 +72,14 @@
   \item elim-resolution, \bold{20}, 30
   \item equality
     \subitem polymorphic, 3
-  \item {\tt eres_inst_tac}, 57
-  \item {\tt eresolve_tac}, 30, 33, 39, 47
+  \item {\tt eres_inst_tac}, 56
+  \item {\tt eresolve_tac}, 30, 33, 39
   \item examples
     \subitem of deriving rules, 41
-    \subitem of induction, 57, 58
-    \subitem of simplification, 60
+    \subitem of induction, 56, 57
+    \subitem of simplification, 59
     \subitem of tacticals, 37
-    \subitem of theories, 48, 50--54, 56, 61
+    \subitem of theories, 47, 49--53, 55, 60
     \subitem propositional, 17, 31, 33
     \subitem with quantifiers, 18, 34, 36, 38
   \item {\tt exE} theorem, 38
@@ -97,20 +96,20 @@
 
   \indexspace
 
-  \item {\tt goal}, 30, 41, 46
-  \item {\tt goalw}, 44--46
+  \item {\tt Goal}, 30, 41
+  \item {\tt Goalw}, 44
 
   \indexspace
 
-  \item {\tt has_fewer_prems}, 64
+  \item {\tt has_fewer_prems}, 63
   \item higher-order logic, 4
 
   \indexspace
 
   \item identifiers, 24
   \item {\tt impI} theorem, 31, 44
-  \item infixes, 52
-  \item instantiation, 57--60
+  \item infixes, 51
+  \item instantiation, 56--59
   \item Isabelle
     \subitem object-logics supported, i
     \subitem overview, i
@@ -136,31 +135,31 @@
   \item meta-implication, \bold{5}, 7, 26
   \item meta-quantifiers, \bold{5}, 8, 26
   \item meta-rewriting, 43
-  \item mixfix declarations, 52, 53, 56
+  \item mixfix declarations, 51, 52, 55
   \item ML, i
-  \item {\tt ML} section, 47
+  \item {\tt ML} section, 46
   \item {\tt mp} theorem, 27, 28
 
   \indexspace
 
-  \item {\tt Nat} theory, 56
+  \item {\tt Nat} theory, 55
   \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
+  \item {\tt notE} theorem, 57
+  \item {\tt notI} theorem, \bold{44}, 57
 
   \indexspace
 
   \item {\tt o} type, 3, 4
   \item {\tt ORELSE}, 38
-  \item overloading, \bold{4}, 53
+  \item overloading, \bold{4}, 52
 
   \indexspace
 
   \item parameters, \bold{8}, 34
     \subitem lifting over, 15
-  \item {\tt Prolog} theory, 61
-  \item Prolog interpreter, \bold{61}
+  \item {\tt Prolog} theory, 60
+  \item Prolog interpreter, \bold{60}
   \item proof state, 16
   \item proofs
     \subitem commands for, 30
@@ -170,33 +169,33 @@
   \item {\tt prth}, 27
   \item {\tt prthq}, 27, 29
   \item {\tt prths}, 27
-  \item {\tt Pure} theory, 47
+  \item {\tt Pure} theory, 46
 
   \indexspace
 
-  \item {\tt qed}, 31, 42, 46
+  \item {\tt qed}, 31, 43
   \item quantifiers, 5, 8, 34
 
   \indexspace
 
   \item {\tt read_instantiate}, 29
   \item {\tt refl} theorem, 29
-  \item {\tt REPEAT}, 34, 38, 62, 64
-  \item {\tt res_inst_tac}, 57, 60
+  \item {\tt REPEAT}, 34, 38, 61, 63
+  \item {\tt res_inst_tac}, 56, 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
+    \subitem with instantiation, 56
+  \item {\tt resolve_tac}, 30, 31, 57
   \item {\tt result}, 31
-  \item {\tt rewrite_goals_tac}, 44
-  \item {\tt rewrite_rule}, 45, 46
+  \item {\tt rewrite_goals_tac}, 44, 45
+  \item {\tt rewrite_rule}, 45
   \item {\tt RL}, 29
   \item {\tt RLN}, 29
-  \item {\tt RS}, 27, 29, 46
+  \item {\tt RS}, 27, 29
   \item {\tt RSN}, 27, 29
   \item rules
-    \subitem declaring, 48
+    \subitem declaring, 47
     \subitem derived, 13, \bold{22}, 41, 43
     \subitem destruction, 21
     \subitem elimination, 21
@@ -206,18 +205,18 @@
   \indexspace
 
   \item search
-    \subitem depth-first, 63
+    \subitem depth-first, 62
   \item signatures, \bold{9}
-  \item {\tt Simp_tac}, 60
-  \item simplification, 60
-  \item simplification sets, 60
+  \item {\tt Simp_tac}, 59
+  \item simplification, 59
+  \item simplification sets, 59
   \item sort constraints, 25
   \item sorts, \bold{5}
   \item {\tt spec} theorem, 28, 36, 38
   \item {\tt standard}, 27
   \item substitution, \bold{8}
-  \item {\tt Suc_inject}, 58
-  \item {\tt Suc_neq_0}, 58
+  \item {\tt Suc_inject}, 57
+  \item {\tt Suc_neq_0}, 57
   \item syntax
     \subitem of types and terms, 25
 
@@ -234,16 +233,16 @@
     \subitem basic operations on, \bold{27}
     \subitem printing of, 27
   \item theories, \bold{9}
-    \subitem defining, 47--57
+    \subitem defining, 46--56
   \item {\tt thm} ML type, 27
-  \item {\tt topthm}, 42
+  \item {\tt topthm}, 43
   \item {\tt Trueprop} constant, 6, 7, 26
   \item type constraints, 25
   \item type constructors, 1
   \item type identifiers, 25
-  \item type synonyms, \bold{51}
+  \item type synonyms, \bold{50}
   \item types
-    \subitem declaring, \bold{49}
+    \subitem declaring, \bold{48}
     \subitem function, 1
     \subitem higher, \bold{5}
     \subitem polymorphic, \bold{3}
@@ -254,11 +253,11 @@
 
   \item {\tt undo}, 31
   \item unification
-    \subitem higher-order, \bold{11}, 58
+    \subitem higher-order, \bold{11}, 57
     \subitem incompleteness of, 11
   \item unknowns, 10, 25, 34
     \subitem function, \bold{11}, 29, 34
-  \item {\tt use_thy}, \bold{47, 48}
+  \item {\tt use_thy}, \bold{46, 47}
 
   \indexspace