diff -r d8205bb279a7 -r 216d6ed87399 doc-src/Intro/intro.ind
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Intro/intro.ind	Wed Nov 10 05:06:55 1993 +0100
@@ -0,0 +1,251 @@
+\begin{theindex}
+
+  \item $\Forall$, \bold{5}, 7
+  \item $\Imp$, \bold{5}
+  \item $\To$, \bold{1}, \bold{3}
+  \item $\equiv$, \bold{5}
+
+  \indexspace
+
+  \item {\tt allI}, 35
+  \item arities
+    \subitem declaring, 3, \bold{46}
+  \item {\tt asm_simp_tac}, 55
+  \item associativity of addition, 54
+  \item {\tt assume_tac}, \bold{27}, 29, 30, 35, 43, 44
+  \item assumptions, 6
+
+  \indexspace
+
+  \item {\tt ba}, \bold{28}
+  \item {\tt back}, 54, 57
+  \item backtracking, 57
+  \item {\tt bd}, \bold{28}
+  \item {\tt be}, \bold{28}
+  \item {\tt br}, \bold{28}
+  \item {\tt by}, \bold{28}
+
+  \indexspace
+
+  \item {\tt choplev}, 34, 35, 59
+  \item classes, \bold{3}
+    \subitem built-in, \bold{23}
+  \item classical reasoning package, 36
+  \item classical sets, \bold{36}
+  \item {\tt conjunct1}, 25
+  \item constants
+    \subitem declaring, \bold{45}
+
+  \indexspace
+
+  \item definitions, \bold{5}
+    \subitem reasoning about, \bold{40}
+  \item {\tt DEPTH_FIRST}, 59
+  \item destruct-resolution, \bold{20}
+  \item destruction rules, \bold{20}
+  \item {\tt disjE}, 29
+  \item {\tt dres_inst_tac}, \bold{52}
+  \item {\tt dresolve_tac}, \bold{28}, 30, 33, 36
+
+  \indexspace
+
+  \item eigenvariables, \see{parameters}{7}
+  \item elim-resolution, \bold{18}
+  \item equality
+    \subitem meta-level, \bold{5}
+  \item {\tt eres_inst_tac}, \bold{52}
+  \item {\tt eresolve_tac}, \bold{27}, 30, 36, 43, 44
+  \item examples
+    \subitem of deriving rules, 38
+    \subitem of induction, 52, 53
+    \subitem of rewriting, 54
+    \subitem of tacticals, 35
+    \subitem of theories, 45--51, 56
+    \subitem propositional, 16, 28, 30
+    \subitem with quantifiers, 17, 31, 33, 35
+  \item {\tt exE}, 35
+
+  \indexspace
+
+  \item {\tt FalseE}, 42
+  \item {\tt fast_tac}, 36, 37
+  \item flex-flex equations, \bold{5}, 23, \bold{26}
+  \item {\tt flexflex_rule}, 26
+  \item {\tt FOL}, 56
+  \item {\tt FOL.thy}, 28
+  \item folding, \bold{40}
+
+  \indexspace
+
+  \item {\tt goal}, \bold{28}, 38, 39, 41--43
+  \item {\tt goalw}, 42, 43
+
+  \indexspace
+
+  \item {\tt has_fewer_prems}, 59
+
+  \indexspace
+
+  \item identifiers, \bold{22}
+  \item imitation, \bold{10}
+  \item {\tt impI}, 29, 41
+  \item implication
+    \subitem meta-level, \bold{5}
+  \item infix operators, \bold{47}
+  \item instantiation
+    \subitem explicit, \bold{52}
+  \item Isabelle
+    \subitem definitions in, 40
+    \subitem formalizing rules, \bold{5}
+    \subitem formalizing syntax, \bold{1}
+    \subitem getting started, 22
+    \subitem object-logics supported, i
+    \subitem overview, i
+    \subitem proof construction in, \bold{9}
+    \subitem release history, i
+    \subitem syntax of, 23
+
+  \indexspace
+
+  \item LCF, i, 14, 24
+  \item level, \bold{29}
+  \item lifting, \bold{13}
+    \subitem over assumptions, \bold{13}
+    \subitem over parameters, \bold{13}
+  \item {\tt logic}, 23
+
+  \indexspace
+
+  \item main goal, \bold{14}
+  \item major premise, \bold{19}
+  \item {\tt Match}, 39
+  \item meta-formulae
+    \subitem syntax, \bold{23}
+  \item meta-logic, \bold{5}
+  \item mixfix operators, \bold{47}
+  \item ML, i, 22, 25
+  \item {\tt mp}, 25
+
+  \indexspace
+
+  \item {\tt Nat}, \bold{51}
+  \item {\tt Nat.thy}, 53
+  \item {\tt not_def}, 41
+  \item {\tt notE}, \bold{43}, 53
+  \item {\tt notI}, \bold{41}, 53
+
+  \indexspace
+
+  \item {\tt ORELSE}, 35
+  \item overloading, \bold{4}, 48
+
+  \indexspace
+
+  \item parameters, \bold{7}, 31
+  \item printing commands, \bold{25}
+  \item projection, \bold{10}
+  \item {\tt Prolog}, 56
+  \item Prolog interpreter, \bold{55}
+  \item proof
+    \subitem backward, \bold{14}
+    \subitem by assumption, \bold{15}
+    \subitem by induction, 52
+    \subitem commands for, \bold{28}
+    \subitem forward, 20
+  \item proof state, \bold{14}
+  \item {\tt PROP}, 24
+  \item {\tt prop}, 23, 24
+  \item {\tt prth}, \bold{25}
+  \item {\tt prthq}, \bold{25}, 26
+  \item {\tt prths}, \bold{25}
+  \item {\tt Pure}, \bold{44}
+
+  \indexspace
+
+  \item quantifiers
+    \subitem meta-level, \bold{5}
+    \subitem reasoning about, 31
+
+  \indexspace
+
+  \item {\tt read_instantiate}, 27
+  \item refinement, \bold{15}
+    \subitem with instantiation, \bold{52}
+  \item {\tt refl}, 27
+  \item {\tt REPEAT}, 30, 35, 57, 59
+  \item {\tt res_inst_tac}, \bold{52}, 54, 55
+  \item reserved words, \bold{22}
+  \item resolution, \bold{11}
+    \subitem in backward proof, 14
+  \item {\tt resolve_tac}, \bold{27}, 29, 43, 53
+  \item {\tt result}, \bold{28}, 29, 38, 39, 44
+  \item {\tt rewrite_goals_tac}, 41, 42
+  \item {\tt rewrite_rule}, 42, 43
+  \item rewriting
+    \subitem meta-level, 40, \bold{40}
+    \subitem object-level, 54
+  \item {\tt RL}, 27
+  \item {\tt RLN}, 27
+  \item {\tt RS}, \bold{25}, 27, 43
+  \item {\tt RSN}, \bold{25}, 27
+  \item rules
+    \subitem declaring, \bold{45}
+    \subitem derived, 12, \bold{20}, 38, 40
+    \subitem propositional, \bold{6}
+    \subitem quantifier, \bold{7}
+
+  \indexspace
+
+  \item search
+    \subitem depth-first, 58
+  \item signatures, \bold{8}
+  \item {\tt simp_tac}, 55
+  \item simplification set, \bold{54}
+  \item sorts, \bold{4}
+  \item {\tt spec}, 26, 33, 35
+  \item {\tt standard}, \bold{25}
+  \item subgoals, \bold{14}
+  \item substitution, \bold{7}
+  \item {\tt Suc_inject}, 53
+  \item {\tt Suc_neq_0}, 53
+
+  \indexspace
+
+  \item tacticals, \bold{14}, \bold{17}, 35
+  \item Tactics, \bold{14}
+  \item tactics, \bold{17}
+    \subitem basic, \bold{27}
+  \item terms
+    \subitem syntax, \bold{23}
+  \item theorems
+    \subitem basic operations on, \bold{24}
+  \item theories, \bold{8}
+    \subitem defining, 44--52
+  \item {\tt thm}, 24
+  \item {\tt topthm}, 39
+  \item {$Trueprop$}, 6, 7, 9, 23
+  \item type constructors
+    \subitem declaring, \bold{46}
+  \item types, 1
+    \subitem higher, \bold{4}
+    \subitem polymorphic, \bold{3}
+    \subitem simple, \bold{1}
+    \subitem syntax, \bold{23}
+
+  \indexspace
+
+  \item {\tt undo}, \bold{28}
+  \item unfolding, \bold{40}
+  \item unification
+    \subitem higher-order, \bold{10}, 53
+  \item unknowns, \bold{9}, 31
+    \subitem of function type, \bold{11}, 26
+  \item {\tt use_thy}, \bold{44, 45}
+
+  \indexspace
+
+  \item variables
+    \subitem bound, 7
+    \subitem schematic, \see{unknowns}{9}
+
+\end{theindex}