\begin{theindex}
\item {\ptt !!} symbol, 24
\subitem in main goal, 44
\item {\tt\%} symbol, 24
\item {\ptt ::} symbol, 24
\item {\ptt ==} symbol, 24
\item {\ptt ==>} symbol, 24
\item {\ptt =>} symbol, 24
\item {\ptt =?=} symbol, 24
\item {\ptt [} symbol, 24
\item {\ptt [|} symbol, 24
\item {\ptt ]} symbol, 24
\item {\tt\ttlbrace} symbol, 24
\item {\tt\ttrbrace} symbol, 24
\item {\ptt |]} symbol, 24
\indexspace
\item {\ptt allI} theorem, 35
\item arities
\subitem declaring, 4, \bold{46}
\item {\ptt asm_simp_tac}, 56
\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
\indexspace
\item {\ptt ba}, 29
\item {\ptt back}, 54, 55, 58
\item backtracking
\subitem Prolog style, 58
\item {\ptt bd}, 29
\item {\ptt be}, 29
\item {\ptt br}, 29
\item {\ptt by}, 29
\indexspace
\item {\ptt choplev}, 34, 35, 60
\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 polymorphic, 3
\indexspace
\item definitions, 5, \bold{46}
\subitem and derived rules, 41--44
\item {\ptt DEPTH_FIRST}, 59
\item destruct-resolution, 21, 29
\item {\ptt disjE} theorem, 30
\item {\ptt dres_inst_tac}, 53
\item {\ptt dresolve_tac}, 29, 31, 36
\indexspace
\item eigenvariables, \see{parameters}{7}
\item elim-resolution, \bold{19}, 28
\item equality
\subitem polymorphic, 3
\item {\ptt eres_inst_tac}, 53
\item {\ptt eresolve_tac}, 28, 31, 36, 44
\item examples
\subitem of deriving rules, 39
\subitem of induction, 53, 54
\subitem of simplification, 55
\subitem of tacticals, 35
\subitem of theories, 46--52, 57
\subitem propositional, 16, 29, 31
\subitem with quantifiers, 17, 32, 33, 36
\item {\ptt exE} theorem, 36
\indexspace
\item {\ptt FalseE} theorem, 43
\item {\ptt fast_tac}, 37
\item first-order logic, 1
\item flex-flex constraints, 5, 24, \bold{27}
\item {\ptt flexflex_rule}, 27
\item forward proof, 20, 23--29
\item {\ptt fun} type, 1, 4
\item function applications, 1, 7
\indexspace
\item {\ptt goal}, 29, 39, 44
\item {\ptt goalw}, 42--44
\indexspace
\item {\ptt has_fewer_prems}, 60
\item higher-order logic, 4
\indexspace
\item identifiers, 23
\item {\ptt impI} theorem, 30, 42
\item infixes, 48
\item instantiation, 53--56
\item Isabelle
\subitem object-logics supported, i
\subitem overview, i
\subitem release history, i
\indexspace
\item $\lambda$-abstractions, 1, 7, 24
\item $\lambda$-calculus, 1
\item LCF, i
\item LCF system, 15, 25
\item level of a proof, 29
\item lifting, \bold{13}
\item {\ptt logic} class, 3, 6, 24
\indexspace
\item major premise, \bold{20}
\item {\ptt Match} exception, 40
\item meta-assumptions
\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, 52
\item ML, i
\item {\ptt ML} section, 45
\item {\ptt mp} theorem, 26
\indexspace
\item {\ptt Nat} theory, 52
\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
\indexspace
\item {\ptt o} type, 1, 4
\item {\ptt ORELSE}, 35
\item overloading, \bold{4}, 50
\indexspace
\item parameters, \bold{7}, 32
\subitem lifting over, 14
\item {\ptt Prolog} theory, 57
\item Prolog interpreter, \bold{56}
\item proof state, 15
\item proofs
\subitem commands for, 29
\item {\ptt PROP} symbol, 25
\item {\ptt prop} type, 6, 24
\item {\ptt prth}, 26
\item {\ptt prthq}, 26, 27
\item {\ptt prths}, 26
\item {\ptt Pure} theory, 45
\indexspace
\item quantifiers, 5, 7, 32
\indexspace
\item {\ptt read_instantiate}, 28
\item {\ptt refl} theorem, 28
\item {\ptt REPEAT}, 31, 36, 58, 59
\item {\ptt res_inst_tac}, 53, 55
\item reserved words, 23
\item resolution, 10, \bold{11}
\subitem in backward proof, 15
\subitem with instantiation, 53
\item {\ptt resolve_tac}, 28, 30, 43, 54
\item {\ptt result}, 29, 40, 44
\item {\ptt rewrite_goals_tac}, 42
\item {\ptt rewrite_rule}, 43
\item {\ptt RL}, 27, 28
\item {\ptt RLN}, 27
\item {\ptt RS}, 26, 27, 44
\item {\ptt RSN}, 26, 27
\item rules
\subitem declaring, 46
\subitem derived, 12, \bold{21}, 39, 41
\subitem destruction, 20
\subitem elimination, 20
\subitem propositional, 6
\subitem quantifier, 7
\indexspace
\item search
\subitem depth-first, 59
\item signatures, \bold{8}
\item {\ptt simp_tac}, 56
\item simplification, 55
\item simplification sets, 55
\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 syntax
\subitem of types and terms, 24
\indexspace
\item tacticals, \bold{18}, 35
\item tactics, \bold{18}
\subitem assumption, 28
\subitem resolution, 28
\item {\ptt term} class, 3
\item terms
\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
\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 types
\subitem declaring, \bold{46}
\subitem function, 1
\subitem higher, \bold{5}
\subitem polymorphic, \bold{3}
\subitem simple, \bold{1}
\subitem syntax of, 1, \bold{24}
\indexspace
\item {\ptt undo}, 29
\item unification
\subitem higher-order, \bold{10}, 54
\subitem incompleteness of, 11
\item unknowns, 9, 23, 32
\subitem function, \bold{11}, 27, 32
\item {\ptt use_thy}, \bold{45}
\indexspace
\item variables
\subitem bound, 7
\end{theindex}