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