--- a/doc-src/Intro/intro.ind Tue May 03 18:36:18 1994 +0200
+++ b/doc-src/Intro/intro.ind Tue May 03 18:38:28 1994 +0200
@@ -1,251 +1,265 @@
\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
+ \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 {\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}
+ \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 {\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}
+ \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 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
+ \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{18}
+ \item elim-resolution, \bold{19}, 28
\item equality
- \subitem meta-level, \bold{5}
- \item {\tt eres_inst_tac}, \bold{52}
- \item {\tt eresolve_tac}, \bold{27}, 30, 36, 43, 44
+ \subitem polymorphic, 3
+ \item {\ptt eres_inst_tac}, 53
+ \item {\ptt eresolve_tac}, 28, 31, 36, 44
\item examples
- \subitem of deriving rules, 38
- \subitem of induction, 52, 53
- \subitem of rewriting, 54
+ \subitem of deriving rules, 39
+ \subitem of induction, 53, 54
+ \subitem of simplification, 55
\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
+ \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 {\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
+ \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 {\tt has_fewer_prems}, 59
+ \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, \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 identifiers, 23
+ \item {\ptt impI} theorem, 30, 42
+ \item infixes, 48
+ \item instantiation, 53--56
\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 $\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}
- \subitem over assumptions, \bold{13}
- \subitem over parameters, \bold{13}
- \item {\tt logic}, 23
+ \item {\ptt logic} class, 3, 6, 24
\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
+ \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 {\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
+ \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 {\tt ORELSE}, 35
- \item overloading, \bold{4}, 48
+ \item {\ptt o} type, 1, 4
+ \item {\ptt ORELSE}, 35
+ \item overloading, \bold{4}, 50
\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}
+ \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 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 {\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, \bold{45}
- \subitem derived, 12, \bold{20}, 38, 40
- \subitem propositional, \bold{6}
- \subitem quantifier, \bold{7}
+ \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, 58
+ \subitem depth-first, 59
\item signatures, \bold{8}
- \item {\tt simp_tac}, 55
- \item simplification set, \bold{54}
+ \item {\ptt simp_tac}, 56
+ \item simplification, 55
+ \item simplification sets, 55
+ \item sort constraints, 24
\item sorts, \bold{4}
- \item {\tt spec}, 26, 33, 35
- \item {\tt standard}, \bold{25}
- \item subgoals, \bold{14}
+ \item {\ptt spec} theorem, 26, 34, 35
+ \item {\ptt standard}, 26
\item substitution, \bold{7}
- \item {\tt Suc_inject}, 53
- \item {\tt Suc_neq_0}, 53
+ \item {\ptt Suc_inject}, 54
+ \item {\ptt Suc_neq_0}, 54
+ \item syntax
+ \subitem of types and terms, 24
\indexspace
- \item tacticals, \bold{14}, \bold{17}, 35
- \item Tactics, \bold{14}
- \item tactics, \bold{17}
- \subitem basic, \bold{27}
+ \item tacticals, \bold{18}, 35
+ \item tactics, \bold{18}
+ \subitem assumption, 28
+ \subitem resolution, 28
+ \item {\ptt term} class, 3
\item terms
- \subitem syntax, \bold{23}
+ \subitem syntax of, 1, \bold{24}
\item theorems
- \subitem basic operations on, \bold{24}
+ \subitem basic operations on, \bold{25}
+ \subitem printing of, 25
\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 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}
- \item types, 1
- \subitem higher, \bold{4}
+ \subitem function, 1
+ \subitem higher, \bold{5}
\subitem polymorphic, \bold{3}
\subitem simple, \bold{1}
- \subitem syntax, \bold{23}
+ \subitem syntax of, 1, \bold{24}
\indexspace
- \item {\tt undo}, \bold{28}
- \item unfolding, \bold{40}
+ \item {\ptt undo}, 29
\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}
+ \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
- \subitem schematic, \see{unknowns}{9}
\end{theindex}