doc-src/Intro/intro.ind

added SCANNER;
changed scan_any: no longer uses take_prefix;

\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}