doc-src/Intro/intro.ind

added this stuff;

\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{47}
  \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}, 55, 59
  \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}, 60
  \item destruct-resolution, 21, 29
  \item {\ptt disjE} theorem, 30
  \item {\ptt dres_inst_tac}, 54
  \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}, 54
  \item {\ptt eresolve_tac}, 28, 31, 36, 44
  \item examples
    \subitem of deriving rules, 39
    \subitem of induction, 54, 55
    \subitem of simplification, 56
    \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, 49
  \item instantiation, 53--57
  \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, 50, 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{57}
  \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, 60
  \item {\ptt res_inst_tac}, 53, 56
  \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, 55
  \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, 56
  \item simplification sets, 56
  \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{47}
    \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}, 55
    \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}