diff -r 567c093297e6 -r 4bbeb1f58a23 doc-src/Intro/intro.ind
--- a/doc-src/Intro/intro.ind	Fri May 16 15:50:24 1997 +0200
+++ b/doc-src/Intro/intro.ind	Fri May 16 15:51:11 1997 +0200
@@ -29,12 +29,12 @@
     \subitem of main goal, 41
     \subitem use of, 16, 28
   \item axioms
-    \subitem Peano, 54
+    \subitem Peano, 55
 
   \indexspace
 
   \item {\tt ba}, 31
-  \item {\tt back}, 59, 62
+  \item {\tt back}, 59, 63
   \item backtracking
     \subitem Prolog style, 62
   \item {\tt bd}, 31
@@ -45,7 +45,7 @@
 
   \indexspace
 
-  \item {\tt choplev}, 37, 64
+  \item {\tt choplev}, 37, 65
   \item classes, 3
     \subitem built-in, \bold{25}
   \item classical reasoner, 39
@@ -53,7 +53,7 @@
   \item constants, 3
     \subitem clashes with variables, 9
     \subitem declaring, \bold{48}
-    \subitem overloaded, 53
+    \subitem overloaded, 54
     \subitem polymorphic, 3
   \item {\tt CPure} theory, 47
 
@@ -78,9 +78,9 @@
   \item examples
     \subitem of deriving rules, 41
     \subitem of induction, 57, 58
-    \subitem of simplification, 59
+    \subitem of simplification, 60
     \subitem of tacticals, 37
-    \subitem of theories, 48, 50--55, 61
+    \subitem of theories, 48, 50--54, 56, 61
     \subitem propositional, 17, 31, 32
     \subitem with quantifiers, 18, 34, 35, 38
   \item {\tt exE} theorem, 38
@@ -143,11 +143,11 @@
 
   \indexspace
 
-  \item {\tt Nat} theory, 55
+  \item {\tt Nat} theory, 56
   \item {\tt nat} type, 3
   \item {\tt not_def} theorem, 44
-  \item {\tt notE} theorem, \bold{45}, 57
-  \item {\tt notI} theorem, \bold{44}, 57
+  \item {\tt notE} theorem, \bold{45}, 58
+  \item {\tt notI} theorem, \bold{44}, 58
 
   \indexspace
 
@@ -160,7 +160,7 @@
   \item parameters, \bold{8}, 34
     \subitem lifting over, 15
   \item {\tt Prolog} theory, 61
-  \item Prolog interpreter, \bold{60}
+  \item Prolog interpreter, \bold{61}
   \item proof state, 16
   \item proofs
     \subitem commands for, 30
@@ -181,7 +181,7 @@
   \item {\tt read_instantiate}, 29
   \item {\tt refl} theorem, 29
   \item {\tt REPEAT}, 33, 38, 62, 64
-  \item {\tt res_inst_tac}, 57, 59
+  \item {\tt res_inst_tac}, 57, 60
   \item reserved words, 24
   \item resolution, 10, \bold{12}
     \subitem in backward proof, 15
@@ -208,8 +208,8 @@
     \subitem depth-first, 63
   \item signatures, \bold{9}
   \item {\tt Simp_tac}, 60
-  \item simplification, 59
-  \item simplification sets, 59
+  \item simplification, 60
+  \item simplification sets, 60
   \item sort constraints, 25
   \item sorts, \bold{5}
   \item {\tt spec} theorem, 28, 36, 37
@@ -233,7 +233,7 @@
     \subitem basic operations on, \bold{27}
     \subitem printing of, 27
   \item theories, \bold{9}
-    \subitem defining, 47--56
+    \subitem defining, 47--57
   \item {\tt thm} ML type, 27
   \item {\tt topthm}, 42
   \item {\tt Trueprop} constant, 6, 7, 25