doc-src/Intro/intro.ind
author wenzelm
Thu, 17 Jul 1997 15:03:38 +0200
changeset 3524 c02cb15830de
parent 3492 88e786024079
child 4802 c15f46833f7a
permissions -rw-r--r--
fixed EqI meta rule;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     1
\begin{theindex}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     2
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
     3
  \item {\tt !!} symbol, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
     4
    \subitem in main goal, 46
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
     5
  \item {\tt\%} symbol, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
     6
  \item {\tt ::} symbol, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
     7
  \item {\tt ==} symbol, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
     8
  \item {\tt ==>} symbol, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
     9
  \item {\tt =>} symbol, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    10
  \item {\tt =?=} symbol, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    11
  \item {\tt [} symbol, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    12
  \item {\tt [|} symbol, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    13
  \item {\tt ]} symbol, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    14
  \item {\tt\ttlbrace} symbol, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    15
  \item {\tt\ttrbrace} symbol, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    16
  \item {\tt |]} symbol, 25
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    17
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    18
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    19
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    20
  \item {\tt allI} theorem, 37
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    21
  \item arities
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    22
    \subitem declaring, 4, \bold{49}
3114
943f25285a3e fixed simplifier ex;
wenzelm
parents: 3104
diff changeset
    23
  \item {\tt Asm_simp_tac}, 60
3104
wenzelm
parents: 3096
diff changeset
    24
  \item {\tt assume_tac}, 30, 32, 37, 47
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    25
  \item assumptions
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    26
    \subitem deleting, 20
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    27
    \subitem discharge of, 7
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    28
    \subitem lifting over, 14
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    29
    \subitem of main goal, 41
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    30
    \subitem use of, 16, 28
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    31
  \item axioms
3213
wenzelm
parents: 3129
diff changeset
    32
    \subitem Peano, 55
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    33
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    34
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    35
3104
wenzelm
parents: 3096
diff changeset
    36
  \item {\tt ba}, 31
3213
wenzelm
parents: 3129
diff changeset
    37
  \item {\tt back}, 59, 63
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    38
  \item backtracking
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    39
    \subitem Prolog style, 62
3104
wenzelm
parents: 3096
diff changeset
    40
  \item {\tt bd}, 31
wenzelm
parents: 3096
diff changeset
    41
  \item {\tt be}, 31
3129
wenzelm
parents: 3114
diff changeset
    42
  \item {\tt Blast_tac}, 39
3104
wenzelm
parents: 3096
diff changeset
    43
  \item {\tt br}, 31
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    44
  \item {\tt by}, 30
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    45
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    46
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    47
3213
wenzelm
parents: 3129
diff changeset
    48
  \item {\tt choplev}, 37, 65
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    49
  \item classes, 3
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    50
    \subitem built-in, \bold{25}
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    51
  \item classical reasoner, 39
3104
wenzelm
parents: 3096
diff changeset
    52
  \item {\tt conjunct1} theorem, 28
wenzelm
parents: 3096
diff changeset
    53
  \item constants, 3
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    54
    \subitem clashes with variables, 9
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    55
    \subitem declaring, \bold{48}
3213
wenzelm
parents: 3129
diff changeset
    56
    \subitem overloaded, 54
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    57
    \subitem polymorphic, 3
3104
wenzelm
parents: 3096
diff changeset
    58
  \item {\tt CPure} theory, 47
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    59
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    60
  \indexspace
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    61
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    62
  \item definitions, 6, \bold{48}
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    63
    \subitem and derived rules, 43--46
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    64
  \item {\tt DEPTH_FIRST}, 64
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    65
  \item destruct-resolution, 22, 30
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    66
  \item {\tt disjE} theorem, 31
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    67
  \item {\tt dres_inst_tac}, 57
3104
wenzelm
parents: 3096
diff changeset
    68
  \item {\tt dresolve_tac}, 30, 32, 33, 38
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    69
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    70
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    71
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    72
  \item eigenvariables, \see{parameters}{8}
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    73
  \item elim-resolution, \bold{20}, 30
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    74
  \item equality
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    75
    \subitem polymorphic, 3
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    76
  \item {\tt eres_inst_tac}, 57
3104
wenzelm
parents: 3096
diff changeset
    77
  \item {\tt eresolve_tac}, 30, 32, 33, 39, 47
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    78
  \item examples
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    79
    \subitem of deriving rules, 41
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    80
    \subitem of induction, 57, 58
3213
wenzelm
parents: 3129
diff changeset
    81
    \subitem of simplification, 60
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    82
    \subitem of tacticals, 37
3213
wenzelm
parents: 3129
diff changeset
    83
    \subitem of theories, 48, 50--54, 56, 61
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    84
    \subitem propositional, 17, 31, 32
3104
wenzelm
parents: 3096
diff changeset
    85
    \subitem with quantifiers, 18, 34, 35, 38
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    86
  \item {\tt exE} theorem, 38
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    87
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    88
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    89
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    90
  \item {\tt FalseE} theorem, 45
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    91
  \item first-order logic, 1
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    92
  \item flex-flex constraints, 6, 25, \bold{28}
3104
wenzelm
parents: 3096
diff changeset
    93
  \item {\tt flexflex_rule}, 29
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    94
  \item forward proof, 21, 24--30
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    95
  \item {\tt fun} type, 1, 4
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
    96
  \item function applications, 1, 8
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    97
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    98
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    99
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   100
  \item {\tt goal}, 30, 41, 46
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   101
  \item {\tt goalw}, 44--46
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   102
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   103
  \indexspace
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   104
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   105
  \item {\tt has_fewer_prems}, 64
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   106
  \item higher-order logic, 4
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   107
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   108
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   109
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   110
  \item identifiers, 24
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   111
  \item {\tt impI} theorem, 31, 44
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   112
  \item infixes, 52
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   113
  \item instantiation, 57--60
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   114
  \item Isabelle
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   115
    \subitem object-logics supported, i
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   116
    \subitem overview, i
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   117
    \subitem release history, i
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   118
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   119
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   120
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   121
  \item $\lambda$-abstractions, 1, 8, 25
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   122
  \item $\lambda$-calculus, 1
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   123
  \item LCF, i
3104
wenzelm
parents: 3096
diff changeset
   124
  \item LCF system, 15, 27
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   125
  \item level of a proof, 31
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   126
  \item lifting, \bold{14}
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   127
  \item {\tt logic} class, 3, 6, 25
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   128
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   129
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   130
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   131
  \item major premise, \bold{21}
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   132
  \item {\tt Match} exception, 42
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   133
  \item meta-assumptions
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   134
    \subitem syntax of, 22
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   135
  \item meta-equality, \bold{5}, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   136
  \item meta-implication, \bold{5}, 7, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   137
  \item meta-quantifiers, \bold{5}, 8, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   138
  \item meta-rewriting, 43
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   139
  \item mixfix declarations, 52, 53, 56
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   140
  \item ML, i
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   141
  \item {\tt ML} section, 47
3104
wenzelm
parents: 3096
diff changeset
   142
  \item {\tt mp} theorem, 27, 28
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   143
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   144
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   145
3213
wenzelm
parents: 3129
diff changeset
   146
  \item {\tt Nat} theory, 56
3104
wenzelm
parents: 3096
diff changeset
   147
  \item {\tt nat} type, 3
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   148
  \item {\tt not_def} theorem, 44
3213
wenzelm
parents: 3129
diff changeset
   149
  \item {\tt notE} theorem, \bold{45}, 58
wenzelm
parents: 3129
diff changeset
   150
  \item {\tt notI} theorem, \bold{44}, 58
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   151
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   152
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   153
3104
wenzelm
parents: 3096
diff changeset
   154
  \item {\tt o} type, 3, 4
wenzelm
parents: 3096
diff changeset
   155
  \item {\tt ORELSE}, 38
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   156
  \item overloading, \bold{4}, 53
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   157
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   158
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   159
3104
wenzelm
parents: 3096
diff changeset
   160
  \item parameters, \bold{8}, 34
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   161
    \subitem lifting over, 15
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   162
  \item {\tt Prolog} theory, 61
3213
wenzelm
parents: 3129
diff changeset
   163
  \item Prolog interpreter, \bold{61}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   164
  \item proof state, 16
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   165
  \item proofs
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   166
    \subitem commands for, 30
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   167
  \item {\tt PROP} symbol, 26
3492
88e786024079 Automatic update
paulson
parents: 3213
diff changeset
   168
  \item {\textit {prop}} type, 25, 26
88e786024079 Automatic update
paulson
parents: 3213
diff changeset
   169
  \item {\tt prop} type, 6
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   170
  \item {\tt prth}, 27
3104
wenzelm
parents: 3096
diff changeset
   171
  \item {\tt prthq}, 27, 29
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   172
  \item {\tt prths}, 27
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   173
  \item {\tt Pure} theory, 47
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   174
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   175
  \indexspace
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   176
3104
wenzelm
parents: 3096
diff changeset
   177
  \item {\tt qed}, 31, 42, 46
wenzelm
parents: 3096
diff changeset
   178
  \item quantifiers, 5, 8, 34
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   179
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   180
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   181
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   182
  \item {\tt read_instantiate}, 29
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   183
  \item {\tt refl} theorem, 29
3104
wenzelm
parents: 3096
diff changeset
   184
  \item {\tt REPEAT}, 33, 38, 62, 64
3213
wenzelm
parents: 3129
diff changeset
   185
  \item {\tt res_inst_tac}, 57, 60
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   186
  \item reserved words, 24
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   187
  \item resolution, 10, \bold{12}
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   188
    \subitem in backward proof, 15
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   189
    \subitem with instantiation, 57
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   190
  \item {\tt resolve_tac}, 30, 31, 46, 58
3104
wenzelm
parents: 3096
diff changeset
   191
  \item {\tt result}, 31
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   192
  \item {\tt rewrite_goals_tac}, 44
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   193
  \item {\tt rewrite_rule}, 45, 46
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   194
  \item {\tt RL}, 29
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   195
  \item {\tt RLN}, 29
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   196
  \item {\tt RS}, 27, 29, 46
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   197
  \item {\tt RSN}, 27, 29
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   198
  \item rules
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   199
    \subitem declaring, 48
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   200
    \subitem derived, 13, \bold{22}, 41, 43
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   201
    \subitem destruction, 21
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   202
    \subitem elimination, 21
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   203
    \subitem propositional, 6
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   204
    \subitem quantifier, 8
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   205
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   206
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   207
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   208
  \item search
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   209
    \subitem depth-first, 63
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   210
  \item signatures, \bold{9}
3114
943f25285a3e fixed simplifier ex;
wenzelm
parents: 3104
diff changeset
   211
  \item {\tt Simp_tac}, 60
3213
wenzelm
parents: 3129
diff changeset
   212
  \item simplification, 60
wenzelm
parents: 3129
diff changeset
   213
  \item simplification sets, 60
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   214
  \item sort constraints, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   215
  \item sorts, \bold{5}
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   216
  \item {\tt spec} theorem, 28, 36, 37
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   217
  \item {\tt standard}, 27
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   218
  \item substitution, \bold{8}
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   219
  \item {\tt Suc_inject}, 58
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   220
  \item {\tt Suc_neq_0}, 58
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   221
  \item syntax
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   222
    \subitem of types and terms, 25
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   223
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   224
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   225
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   226
  \item tacticals, \bold{19}, 37
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   227
  \item tactics, \bold{19}
3104
wenzelm
parents: 3096
diff changeset
   228
    \subitem assumption, 30
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   229
    \subitem resolution, 30
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   230
  \item {\tt term} class, 3
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   231
  \item terms
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   232
    \subitem syntax of, 1, \bold{25}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   233
  \item theorems
3104
wenzelm
parents: 3096
diff changeset
   234
    \subitem basic operations on, \bold{27}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   235
    \subitem printing of, 27
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   236
  \item theories, \bold{9}
3213
wenzelm
parents: 3129
diff changeset
   237
    \subitem defining, 47--57
3104
wenzelm
parents: 3096
diff changeset
   238
  \item {\tt thm} ML type, 27
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   239
  \item {\tt topthm}, 42
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   240
  \item {\tt Trueprop} constant, 6, 7, 25
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   241
  \item type constraints, 25
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   242
  \item type constructors, 1
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   243
  \item type identifiers, 24
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   244
  \item type synonyms, \bold{51}
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   245
  \item types
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   246
    \subitem declaring, \bold{49}
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   247
    \subitem function, 1
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   248
    \subitem higher, \bold{5}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   249
    \subitem polymorphic, \bold{3}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   250
    \subitem simple, \bold{1}
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   251
    \subitem syntax of, 1, \bold{25}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   252
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   253
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   254
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   255
  \item {\tt undo}, 30
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   256
  \item unification
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   257
    \subitem higher-order, \bold{11}, 58
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
   258
    \subitem incompleteness of, 11
3104
wenzelm
parents: 3096
diff changeset
   259
  \item unknowns, 10, 24, 34
wenzelm
parents: 3096
diff changeset
   260
    \subitem function, \bold{11}, 28, 34
wenzelm
parents: 3096
diff changeset
   261
  \item {\tt use_thy}, \bold{47, 48}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   262
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   263
  \indexspace
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   264
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   265
  \item variables
3096
ccc2c92bb232 Updated to LaTeX 2e
berghofe
parents: 2977
diff changeset
   266
    \subitem bound, 8
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   267
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   268
\end{theindex}