\begin{theindex}
\item {\ptt !!} symbol, 25
\subitem in main goal, 46
\item {\tt\%} symbol, 25
\item {\ptt ::} symbol, 25
\item {\ptt ==} symbol, 25
\item {\ptt ==>} symbol, 25
\item {\ptt =>} symbol, 25
\item {\ptt =?=} symbol, 25
\item {\ptt [} symbol, 25
\item {\ptt [|} symbol, 25
\item {\ptt ]} symbol, 25
\item {\tt\ttlbrace} symbol, 25
\item {\tt\ttrbrace} symbol, 25
\item {\ptt |]} symbol, 25
\indexspace
\item {\ptt allI} theorem, 37
\item arities
\subitem declaring, 4, \bold{49}
\item {\ptt asm_simp_tac}, 60
\item {\ptt assume_tac}, 29, 31, 37, 47
\item assumptions
\subitem deleting, 20
\subitem discharge of, 7
\subitem lifting over, 14
\subitem of main goal, 41
\subitem use of, 16, 28
\item axioms
\subitem Peano, 54
\indexspace
\item {\ptt ba}, 30
\item {\ptt back}, 59, 62
\item backtracking
\subitem Prolog style, 62
\item {\ptt bd}, 30
\item {\ptt be}, 30
\item {\ptt br}, 30
\item {\ptt by}, 30
\indexspace
\item {\ptt choplev}, 36, 37, 64
\item classes, 3
\subitem built-in, \bold{25}
\item classical reasoner, 39
\item {\ptt conjunct1} theorem, 27
\item constants, 1
\subitem clashes with variables, 9
\subitem declaring, \bold{48}
\subitem overloaded, 53
\subitem polymorphic, 3
\indexspace
\item definitions, 6, \bold{48}
\subitem and derived rules, 43--46
\item {\ptt DEPTH_FIRST}, 64
\item destruct-resolution, 22, 30
\item {\ptt disjE} theorem, 31
\item {\ptt dres_inst_tac}, 57
\item {\ptt dresolve_tac}, 30, 32, 38
\indexspace
\item eigenvariables, \see{parameters}{8}
\item elim-resolution, \bold{20}, 30
\item equality
\subitem polymorphic, 3
\item {\ptt eres_inst_tac}, 57
\item {\ptt eresolve_tac}, 30, 32, 38, 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
\item {\ptt exE} theorem, 38
\indexspace
\item {\ptt FalseE} theorem, 45
\item {\ptt fast_tac}, 39
\item first-order logic, 1
\item flex-flex constraints, 6, 25, \bold{28}
\item {\ptt flexflex_rule}, 28
\item forward proof, 21, 24--30
\item {\ptt fun} type, 1, 4
\item function applications, 1, 8
\indexspace
\item {\ptt goal}, 30, 41, 46
\item {\ptt goalw}, 44--46
\indexspace
\item {\ptt has_fewer_prems}, 64
\item higher-order logic, 4
\indexspace
\item identifiers, 24
\item {\ptt impI} theorem, 31, 44
\item infixes, 52
\item instantiation, 57--60
\item Isabelle
\subitem object-logics supported, i
\subitem overview, i
\subitem release history, i
\indexspace
\item $\lambda$-abstractions, 1, 8, 25
\item $\lambda$-calculus, 1
\item LCF, i
\item LCF system, 15, 26
\item level of a proof, 31
\item lifting, \bold{14}
\item {\ptt logic} class, 3, 6, 25
\indexspace
\item major premise, \bold{21}
\item {\ptt Match} exception, 42
\item meta-assumptions
\subitem syntax of, 22
\item meta-equality, \bold{5}, 25
\item meta-implication, \bold{5}, 7, 25
\item meta-quantifiers, \bold{5}, 8, 25
\item meta-rewriting, 43
\item mixfix declarations, 52, 53, 56
\item ML, i
\item {\ptt ML} section, 47
\item {\ptt mp} theorem, 27
\indexspace
\item {\ptt Nat} theory, 55
\item {\ptt nat} type, 1, 3
\item {\ptt not_def} theorem, 44
\item {\ptt notE} theorem, \bold{45}, 58
\item {\ptt notI} theorem, \bold{44}, 58
\indexspace
\item {\ptt o} type, 1, 4
\item {\ptt ORELSE}, 37
\item overloading, \bold{4}, 53
\indexspace
\item parameters, \bold{8}, 33
\subitem lifting over, 15
\item {\ptt Prolog} theory, 61
\item Prolog interpreter, \bold{60}
\item proof state, 16
\item proofs
\subitem commands for, 30
\item {\ptt PROP} symbol, 26
\item {\ptt prop} type, 6, 25, 26
\item {\ptt prth}, 27
\item {\ptt prthq}, 27, 28
\item {\ptt prths}, 27
\item {\ptt Pure} theory, 47
\indexspace
\item quantifiers, 5, 8, 33
\indexspace
\item {\ptt read_instantiate}, 29
\item {\ptt refl} theorem, 29
\item {\ptt REPEAT}, 33, 37, 62, 64
\item {\ptt res_inst_tac}, 57, 60
\item reserved words, 24
\item resolution, 10, \bold{12}
\subitem in backward proof, 15
\subitem with instantiation, 57
\item {\ptt resolve_tac}, 30, 31, 46, 58
\item {\ptt result}, 30, 42, 46
\item {\ptt rewrite_goals_tac}, 44
\item {\ptt rewrite_rule}, 45, 46
\item {\ptt RL}, 29
\item {\ptt RLN}, 29
\item {\ptt RS}, 27, 29, 46
\item {\ptt RSN}, 27, 29
\item rules
\subitem declaring, 48
\subitem derived, 13, \bold{22}, 41, 43
\subitem destruction, 21
\subitem elimination, 21
\subitem propositional, 6
\subitem quantifier, 8
\indexspace
\item search
\subitem depth-first, 63
\item signatures, \bold{9}
\item {\ptt simp_tac}, 60
\item simplification, 59
\item simplification sets, 59
\item sort constraints, 25
\item sorts, \bold{5}
\item {\ptt spec} theorem, 28, 36, 37
\item {\ptt standard}, 27
\item substitution, \bold{8}
\item {\ptt Suc_inject}, 58
\item {\ptt Suc_neq_0}, 58
\item syntax
\subitem of types and terms, 25
\indexspace
\item tacticals, \bold{19}, 37
\item tactics, \bold{19}
\subitem assumption, 29
\subitem resolution, 30
\item {\ptt term} class, 3
\item terms
\subitem syntax of, 1, \bold{25}
\item theorems
\subitem basic operations on, \bold{26}
\subitem printing of, 27
\item theories, \bold{9}
\subitem defining, 47--57
\item {\ptt thm} ML type, 26
\item {\ptt topthm}, 42
\item {\ptt Trueprop} constant, 6, 7, 25
\item type constraints, 25
\item type constructors, 1
\item type identifiers, 24
\item type synonyms, \bold{51}
\item types
\subitem declaring, \bold{49}
\subitem function, 1
\subitem higher, \bold{5}
\subitem polymorphic, \bold{3}
\subitem simple, \bold{1}
\subitem syntax of, 1, \bold{25}
\indexspace
\item {\ptt 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 {\ptt use_thy}, \bold{47}
\indexspace
\item variables
\subitem bound, 8
\end{theindex}