src/Doc/Isar_Ref/Outer_Syntax.thy
author wenzelm
Wed Oct 25 13:47:53 2017 +0200 (23 months ago)
changeset 66916 aca50a1572c5
parent 63531 847eefdca90d
child 67448 dbb1f02e667d
permissions -rw-r--r--
more documentation;
wenzelm@61656
     1
(*:maxLineLen=78:*)
wenzelm@61656
     2
wenzelm@27037
     3
theory Outer_Syntax
wenzelm@63531
     4
  imports Main Base
wenzelm@27037
     5
begin
wenzelm@27037
     6
wenzelm@58618
     7
chapter \<open>Outer syntax --- the theory language \label{ch:outer-syntax}\<close>
wenzelm@27037
     8
wenzelm@58618
     9
text \<open>
wenzelm@61662
    10
  The rather generic framework of Isabelle/Isar syntax emerges from three main
wenzelm@61662
    11
  syntactic categories: \<^emph>\<open>commands\<close> of the top-level Isar engine (covering
wenzelm@61662
    12
  theory and proof elements), \<^emph>\<open>methods\<close> for general goal refinements
wenzelm@61662
    13
  (analogous to traditional ``tactics''), and \<^emph>\<open>attributes\<close> for operations on
wenzelm@61662
    14
  facts (within a certain context). Subsequently we give a reference of basic
wenzelm@61662
    15
  syntactic entities underlying Isabelle/Isar syntax in a bottom-up manner.
wenzelm@61662
    16
  Concrete theory and proof language elements will be introduced later on.
wenzelm@27037
    17
wenzelm@61421
    18
  \<^medskip>
wenzelm@61662
    19
  In order to get started with writing well-formed Isabelle/Isar documents,
wenzelm@61662
    20
  the most important aspect to be noted is the difference of \<^emph>\<open>inner\<close> versus
wenzelm@61662
    21
  \<^emph>\<open>outer\<close> syntax. Inner syntax is that of Isabelle types and terms of the
wenzelm@61662
    22
  logic, while outer syntax is that of Isabelle/Isar theory sources
wenzelm@61662
    23
  (specifications and proofs). As a general rule, inner syntax entities may
wenzelm@61662
    24
  occur only as \<^emph>\<open>atomic entities\<close> within outer syntax. For example, the
wenzelm@61662
    25
  string \<^verbatim>\<open>"x + y"\<close> and identifier \<^verbatim>\<open>z\<close> are legal term specifications within a
wenzelm@61662
    26
  theory, while \<^verbatim>\<open>x + y\<close> without quotes is not.
wenzelm@27037
    27
wenzelm@61662
    28
  Printed theory documents usually omit quotes to gain readability (this is a
wenzelm@61662
    29
  matter of {\LaTeX} macro setup, say via \<^verbatim>\<open>\isabellestyle\<close>, see also @{cite
wenzelm@61662
    30
  "isabelle-system"}). Experienced users of Isabelle/Isar may easily
wenzelm@61662
    31
  reconstruct the lost technical information, while mere readers need not care
wenzelm@61662
    32
  about quotes at all.
wenzelm@58618
    33
\<close>
wenzelm@27037
    34
wenzelm@27037
    35
wenzelm@58618
    36
section \<open>Commands\<close>
wenzelm@50213
    37
wenzelm@58618
    38
text \<open>
wenzelm@50213
    39
  \begin{matharray}{rcl}
wenzelm@61493
    40
    @{command_def "print_commands"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
wenzelm@61493
    41
    @{command_def "help"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
wenzelm@50213
    42
  \end{matharray}
wenzelm@50213
    43
wenzelm@55112
    44
  @{rail \<open>
wenzelm@50213
    45
    @@{command help} (@{syntax name} * )
wenzelm@55112
    46
  \<close>}
wenzelm@50213
    47
wenzelm@61439
    48
  \<^descr> @{command "print_commands"} prints all outer syntax keywords
wenzelm@50213
    49
  and commands.
wenzelm@50213
    50
wenzelm@61493
    51
  \<^descr> @{command "help"}~\<open>pats\<close> retrieves outer syntax
wenzelm@50213
    52
  commands according to the specified name patterns.
wenzelm@58618
    53
\<close>
wenzelm@50213
    54
wenzelm@50213
    55
wenzelm@58618
    56
subsubsection \<open>Examples\<close>
wenzelm@50213
    57
wenzelm@61662
    58
text \<open>
wenzelm@61662
    59
  Some common diagnostic commands are retrieved like this (according to usual
wenzelm@61662
    60
  naming conventions):
wenzelm@61662
    61
\<close>
wenzelm@50213
    62
wenzelm@50213
    63
help "print"
wenzelm@50213
    64
help "find"
wenzelm@50213
    65
wenzelm@50213
    66
wenzelm@58618
    67
section \<open>Lexical matters \label{sec:outer-lex}\<close>
wenzelm@27037
    68
wenzelm@61662
    69
text \<open>
wenzelm@61662
    70
  The outer lexical syntax consists of three main categories of syntax tokens:
wenzelm@28775
    71
wenzelm@61662
    72
    \<^enum> \<^emph>\<open>major keywords\<close> --- the command names that are available
wenzelm@61662
    73
    in the present logic session;
wenzelm@28775
    74
wenzelm@61662
    75
    \<^enum> \<^emph>\<open>minor keywords\<close> --- additional literal tokens required
wenzelm@61662
    76
    by the syntax of commands;
wenzelm@27037
    77
wenzelm@61662
    78
    \<^enum> \<^emph>\<open>named tokens\<close> --- various categories of identifiers etc.
wenzelm@28775
    79
wenzelm@61662
    80
  Major keywords and minor keywords are guaranteed to be disjoint. This helps
wenzelm@61662
    81
  user-interfaces to determine the overall structure of a theory text, without
wenzelm@61662
    82
  knowing the full details of command syntax. Internally, there is some
wenzelm@61662
    83
  additional information about the kind of major keywords, which approximates
wenzelm@61662
    84
  the command type (theory command, proof command etc.).
wenzelm@28775
    85
wenzelm@61662
    86
  Keywords override named tokens. For example, the presence of a command
wenzelm@61662
    87
  called \<^verbatim>\<open>term\<close> inhibits the identifier \<^verbatim>\<open>term\<close>, but the string \<^verbatim>\<open>"term"\<close> can
wenzelm@61662
    88
  be used instead. By convention, the outer syntax always allows quoted
wenzelm@61662
    89
  strings in addition to identifiers, wherever a named entity is expected.
wenzelm@28775
    90
wenzelm@61662
    91
  When tokenizing a given input sequence, the lexer repeatedly takes the
wenzelm@61662
    92
  longest prefix of the input that forms a valid token. Spaces, tabs, newlines
wenzelm@61662
    93
  and formfeeds between tokens serve as explicit separators.
wenzelm@28776
    94
wenzelm@61421
    95
  \<^medskip>
wenzelm@61421
    96
  The categories for named tokens are defined once and for all as follows.
wenzelm@27037
    97
wenzelm@28776
    98
  \begin{center}
wenzelm@28775
    99
  \begin{supertabular}{rcl}
wenzelm@63138
   100
    @{syntax_def short_ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\
wenzelm@63138
   101
    @{syntax_def long_ident} & = & \<open>short_ident(\<close>\<^verbatim>\<open>.\<close>\<open>short_ident)\<^sup>+\<close> \\
wenzelm@63138
   102
    @{syntax_def sym_ident} & = & \<open>sym\<^sup>+  |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>short_ident\<close>\<^verbatim>\<open>>\<close> \\
wenzelm@61493
   103
    @{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\
wenzelm@61503
   104
    @{syntax_def float} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat}~~\<open>|\<close>~~\<^verbatim>\<open>-\<close>@{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\
wenzelm@63138
   105
    @{syntax_def term_var} & = & \<^verbatim>\<open>?\<close>\<open>short_ident  |\<close>~~\<^verbatim>\<open>?\<close>\<open>short_ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
wenzelm@63138
   106
    @{syntax_def type_ident} & = & \<^verbatim>\<open>'\<close>\<open>short_ident\<close> \\
wenzelm@63138
   107
    @{syntax_def type_var} & = & \<^verbatim>\<open>?\<close>\<open>type_ident  |\<close>~~\<^verbatim>\<open>?\<close>\<open>type_ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
wenzelm@61503
   108
    @{syntax_def string} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
wenzelm@61503
   109
    @{syntax_def altstring} & = & \<^verbatim>\<open>`\<close> \<open>\<dots>\<close> \<^verbatim>\<open>`\<close> \\
wenzelm@61493
   110
    @{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
wenzelm@61503
   111
    @{syntax_def verbatim} & = & \<^verbatim>\<open>{*\<close> \<open>\<dots>\<close> \<^verbatim>\<open>*}\<close> \\[1ex]
wenzelm@28775
   112
wenzelm@61503
   113
    \<open>letter\<close> & = & \<open>latin  |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>latin\<close>\<^verbatim>\<open>>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>latin latin\<close>\<^verbatim>\<open>>\<close>~~\<open>|  greek  |\<close> \\
wenzelm@61503
   114
    \<open>subscript\<close> & = & \<^verbatim>\<open>\<^sub>\<close> \\
wenzelm@61503
   115
    \<open>quasiletter\<close> & = & \<open>letter  |  digit  |\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>'\<close> \\
wenzelm@61503
   116
    \<open>latin\<close> & = & \<^verbatim>\<open>a\<close>~~\<open>| \<dots> |\<close>~~\<^verbatim>\<open>z\<close>~~\<open>|\<close>~~\<^verbatim>\<open>A\<close>~~\<open>|  \<dots> |\<close>~~\<^verbatim>\<open>Z\<close> \\
wenzelm@61503
   117
    \<open>digit\<close> & = & \<^verbatim>\<open>0\<close>~~\<open>|  \<dots> |\<close>~~\<^verbatim>\<open>9\<close> \\
wenzelm@61503
   118
    \<open>sym\<close> & = & \<^verbatim>\<open>!\<close>~~\<open>|\<close>~~\<^verbatim>\<open>#\<close>~~\<open>|\<close>~~\<^verbatim>\<open>$\<close>~~\<open>|\<close>~~\<^verbatim>\<open>%\<close>~~\<open>|\<close>~~\<^verbatim>\<open>&\<close>~~\<open>|\<close>~~\<^verbatim>\<open>*\<close>~~\<open>|\<close>~~\<^verbatim>\<open>+\<close>~~\<open>|\<close>~~\<^verbatim>\<open>-\<close>~~\<open>|\<close>~~\<^verbatim>\<open>/\<close>~~\<open>|\<close> \\
wenzelm@61503
   119
    & & \<^verbatim>\<open><\<close>~~\<open>|\<close>~~\<^verbatim>\<open>=\<close>~~\<open>|\<close>~~\<^verbatim>\<open>>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>?\<close>~~\<open>|\<close>~~\<^verbatim>\<open>@\<close>~~\<open>|\<close>~~\<^verbatim>\<open>^\<close>~~\<open>|\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>|\<close>~~\<open>|\<close>~~\<^verbatim>\<open>~\<close> \\
wenzelm@61503
   120
    \<open>greek\<close> & = & \<^verbatim>\<open>\<alpha>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<beta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<gamma>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<delta>\<close>~~\<open>|\<close> \\
wenzelm@61503
   121
          &   & \<^verbatim>\<open>\<epsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<zeta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<eta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<theta>\<close>~~\<open>|\<close> \\
wenzelm@61503
   122
          &   & \<^verbatim>\<open>\<iota>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<kappa>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<mu>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<nu>\<close>~~\<open>|\<close> \\
wenzelm@61503
   123
          &   & \<^verbatim>\<open>\<xi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<pi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<rho>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<sigma>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<tau>\<close>~~\<open>|\<close> \\
wenzelm@61503
   124
          &   & \<^verbatim>\<open>\<upsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<phi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<chi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<psi>\<close>~~\<open>|\<close> \\
wenzelm@61503
   125
          &   & \<^verbatim>\<open>\<omega>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Gamma>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Delta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Theta>\<close>~~\<open>|\<close> \\
wenzelm@61503
   126
          &   & \<^verbatim>\<open>\<Lambda>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Xi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Pi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Sigma>\<close>~~\<open>|\<close> \\
wenzelm@61503
   127
          &   & \<^verbatim>\<open>\<Upsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Phi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Psi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Omega>\<close> \\
wenzelm@28775
   128
  \end{supertabular}
wenzelm@28776
   129
  \end{center}
wenzelm@27037
   130
wenzelm@63138
   131
  A @{syntax_ref term_var} or @{syntax_ref type_var} describes an unknown,
wenzelm@63138
   132
  which is internally a pair of base name and index (ML type @{ML_type
wenzelm@63138
   133
  indexname}). These components are either separated by a dot as in \<open>?x.1\<close> or
wenzelm@63138
   134
  \<open>?x7.3\<close> or run together as in \<open>?x1\<close>. The latter form is possible if the base
wenzelm@63138
   135
  name does not end with digits. If the index is 0, it may be dropped
wenzelm@63138
   136
  altogether: \<open>?x\<close> and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the same unknown, with
wenzelm@63138
   137
  basename \<open>x\<close> and index 0.
wenzelm@28778
   138
wenzelm@28778
   139
  The syntax of @{syntax_ref string} admits any characters, including
wenzelm@61662
   140
  newlines; ``\<^verbatim>\<open>"\<close>'' (double-quote) and ``\<^verbatim>\<open>\\<close>'' (backslash) need to be
wenzelm@61662
   141
  escaped by a backslash; arbitrary character codes may be specified as
wenzelm@61662
   142
  ``\<^verbatim>\<open>\\<close>\<open>ddd\<close>'', with three decimal digits. Alternative strings according to
wenzelm@61662
   143
  @{syntax_ref altstring} are analogous, using single back-quotes instead.
wenzelm@28778
   144
wenzelm@58725
   145
  The body of @{syntax_ref verbatim} may consist of any text not containing
wenzelm@61662
   146
  ``\<^verbatim>\<open>*}\<close>''; this allows to include quotes without further escapes, but there
wenzelm@61662
   147
  is no way to escape ``\<^verbatim>\<open>*}\<close>''. Cartouches do not have this limitation.
wenzelm@28778
   148
wenzelm@61662
   149
  A @{syntax_ref cartouche} consists of arbitrary text, with properly balanced
wenzelm@61662
   150
  blocks of ``@{verbatim "\<open>"}~\<open>\<dots>\<close>~@{verbatim "\<close>"}''. Note that the rendering
wenzelm@61662
   151
  of cartouche delimiters is usually like this: ``\<open>\<open> \<dots> \<close>\<close>''.
wenzelm@55033
   152
wenzelm@61662
   153
  Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested, although
wenzelm@61662
   154
  the user-interface might prevent this. Note that this form indicates source
wenzelm@61662
   155
  comments only, which are stripped after lexical analysis of the input. The
wenzelm@61662
   156
  Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are considered as
wenzelm@61662
   157
  part of the text (see \secref{sec:comments}).
wenzelm@27037
   158
wenzelm@61662
   159
  Common mathematical symbols such as \<open>\<forall>\<close> are represented in Isabelle as \<^verbatim>\<open>\<forall>\<close>.
wenzelm@61662
   160
  There are infinitely many Isabelle symbols like this, although proper
wenzelm@61662
   161
  presentation is left to front-end tools such as {\LaTeX} or Isabelle/jEdit.
wenzelm@61662
   162
  A list of predefined Isabelle symbols that work well with these tools is
wenzelm@61662
   163
  given in \appref{app:symbols}. Note that \<^verbatim>\<open>\<lambda>\<close> does not belong to the
wenzelm@61662
   164
  \<open>letter\<close> category, since it is already used differently in the Pure term
wenzelm@61662
   165
  language.
wenzelm@61662
   166
\<close>
wenzelm@27037
   167
wenzelm@27037
   168
wenzelm@58618
   169
section \<open>Common syntax entities\<close>
wenzelm@27037
   170
wenzelm@58618
   171
text \<open>
wenzelm@61662
   172
  We now introduce several basic syntactic entities, such as names, terms, and
wenzelm@61662
   173
  theorem specifications, which are factored out of the actual Isar language
wenzelm@61662
   174
  elements to be described later.
wenzelm@58618
   175
\<close>
wenzelm@27037
   176
wenzelm@27037
   177
wenzelm@58618
   178
subsection \<open>Names\<close>
wenzelm@27037
   179
wenzelm@61662
   180
text \<open>
wenzelm@61662
   181
  Entity @{syntax name} usually refers to any name of types, constants,
wenzelm@62969
   182
  theorems etc.\ Quoted strings provide an escape for non-identifier names or
wenzelm@62969
   183
  those ruled out by outer syntax keywords (e.g.\ quoted \<^verbatim>\<open>"let"\<close>).
wenzelm@27037
   184
wenzelm@55112
   185
  @{rail \<open>
wenzelm@63138
   186
    @{syntax_def name}: @{syntax short_ident} | @{syntax long_ident} |
wenzelm@63138
   187
      @{syntax sym_ident} | @{syntax nat} | @{syntax string}
wenzelm@27037
   188
    ;
wenzelm@60131
   189
    @{syntax_def par_name}: '(' @{syntax name} ')'
wenzelm@55112
   190
  \<close>}
wenzelm@66916
   191
wenzelm@66916
   192
  A @{syntax_def system_name} is like @{syntax name}, but it excludes
wenzelm@66916
   193
  white-space characters and needs to conform to file-name notation.
wenzelm@58618
   194
\<close>
wenzelm@40296
   195
wenzelm@40296
   196
wenzelm@58618
   197
subsection \<open>Numbers\<close>
wenzelm@40296
   198
wenzelm@61662
   199
text \<open>
wenzelm@61662
   200
  The outer lexical syntax (\secref{sec:outer-lex}) admits natural numbers and
wenzelm@61662
   201
  floating point numbers. These are combined as @{syntax int} and @{syntax
wenzelm@61662
   202
  real} as follows.
wenzelm@40296
   203
wenzelm@55112
   204
  @{rail \<open>
wenzelm@42596
   205
    @{syntax_def int}: @{syntax nat} | '-' @{syntax nat}
wenzelm@27037
   206
    ;
wenzelm@42596
   207
    @{syntax_def real}: @{syntax float} | @{syntax int}
wenzelm@55112
   208
  \<close>}
wenzelm@40296
   209
wenzelm@61662
   210
  Note that there is an overlap with the category @{syntax name}, which also
wenzelm@61662
   211
  includes @{syntax nat}.
wenzelm@58618
   212
\<close>
wenzelm@27037
   213
wenzelm@27037
   214
wenzelm@63120
   215
subsection \<open>Embedded content\<close>
wenzelm@63120
   216
wenzelm@63120
   217
text \<open>
wenzelm@63120
   218
  Entity @{syntax embedded} refers to content of other languages: cartouches
wenzelm@63120
   219
  allow arbitrary nesting of sub-languages that respect the recursive
wenzelm@63120
   220
  balancing of cartouche delimiters. Quoted strings are possible as well, but
wenzelm@63120
   221
  require escaped quotes when nested. As a shortcut, tokens that appear as
wenzelm@63120
   222
  plain identifiers in the outer language may be used as inner language
wenzelm@63120
   223
  content without delimiters.
wenzelm@63120
   224
wenzelm@63120
   225
  @{rail \<open>
wenzelm@63120
   226
    @{syntax_def embedded}: @{syntax cartouche} | @{syntax string} |
wenzelm@63138
   227
      @{syntax short_ident} | @{syntax long_ident} | @{syntax sym_ident} |
wenzelm@63138
   228
      @{syntax term_var} | @{syntax type_ident} | @{syntax type_var} | @{syntax nat}
wenzelm@63120
   229
  \<close>}
wenzelm@63120
   230
\<close>
wenzelm@63120
   231
wenzelm@63120
   232
wenzelm@58618
   233
subsection \<open>Comments \label{sec:comments}\<close>
wenzelm@27037
   234
wenzelm@61579
   235
text \<open>
wenzelm@61579
   236
  Large chunks of plain @{syntax text} are usually given @{syntax verbatim},
wenzelm@61579
   237
  i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>, or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For
wenzelm@62969
   238
  convenience, any of the smaller text units conforming to @{syntax name} are
wenzelm@62969
   239
  admitted as well. A marginal @{syntax comment} is of the form \<^verbatim>\<open>--\<close>~@{syntax
wenzelm@62969
   240
  text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur within
wenzelm@62969
   241
  Isabelle/Isar commands.
wenzelm@27037
   242
wenzelm@55112
   243
  @{rail \<open>
wenzelm@63139
   244
    @{syntax_def text}: @{syntax embedded} | @{syntax verbatim}
wenzelm@27037
   245
    ;
wenzelm@61579
   246
    @{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
wenzelm@55112
   247
  \<close>}
wenzelm@58618
   248
\<close>
wenzelm@27037
   249
wenzelm@27037
   250
wenzelm@58618
   251
subsection \<open>Type classes, sorts and arities\<close>
wenzelm@27037
   252
wenzelm@58618
   253
text \<open>
wenzelm@61662
   254
  Classes are specified by plain names. Sorts have a very simple inner syntax,
wenzelm@61662
   255
  which is either a single class name \<open>c\<close> or a list \<open>{c\<^sub>1, \<dots>, c\<^sub>n}\<close> referring
wenzelm@61662
   256
  to the intersection of these classes. The syntax of type arities is given
wenzelm@27037
   257
  directly at the outer level.
wenzelm@27037
   258
wenzelm@55112
   259
  @{rail \<open>
wenzelm@62969
   260
    @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax name} + ','))?
wenzelm@27037
   261
    ;
wenzelm@63140
   262
    @{syntax_def sort}: @{syntax embedded}
wenzelm@27037
   263
    ;
wenzelm@42596
   264
    @{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort}
wenzelm@55112
   265
  \<close>}
wenzelm@58618
   266
\<close>
wenzelm@27037
   267
wenzelm@27037
   268
wenzelm@58618
   269
subsection \<open>Types and terms \label{sec:types-terms}\<close>
wenzelm@27037
   270
wenzelm@58618
   271
text \<open>
wenzelm@61662
   272
  The actual inner Isabelle syntax, that of types and terms of the logic, is
wenzelm@61662
   273
  far too sophisticated in order to be modelled explicitly at the outer theory
wenzelm@61662
   274
  level. Basically, any such entity has to be quoted to turn it into a single
wenzelm@61662
   275
  token (the parsing and type-checking is performed internally later). For
wenzelm@61662
   276
  convenience, a slightly more liberal convention is adopted: quotes may be
wenzelm@61662
   277
  omitted for any type or term that is already atomic at the outer level. For
wenzelm@61662
   278
  example, one may just write \<^verbatim>\<open>x\<close> instead of quoted \<^verbatim>\<open>"x"\<close>. Note that
wenzelm@61662
   279
  symbolic identifiers (e.g.\ \<^verbatim>\<open>++\<close> or \<open>\<forall>\<close> are available as well, provided
wenzelm@61662
   280
  these have not been superseded by commands or other keywords already (such
wenzelm@61662
   281
  as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
wenzelm@27037
   282
wenzelm@55112
   283
  @{rail \<open>
wenzelm@63137
   284
    @{syntax_def type}: @{syntax embedded}
wenzelm@27037
   285
    ;
wenzelm@63137
   286
    @{syntax_def term}: @{syntax embedded}
wenzelm@27037
   287
    ;
wenzelm@63137
   288
    @{syntax_def prop}: @{syntax embedded}
wenzelm@55112
   289
  \<close>}
wenzelm@27037
   290
wenzelm@59853
   291
  Positional instantiations are specified as a sequence of terms, or the
wenzelm@61493
   292
  placeholder ``\<open>_\<close>'' (underscore), which means to skip a position.
wenzelm@27037
   293
wenzelm@55112
   294
  @{rail \<open>
wenzelm@42596
   295
    @{syntax_def inst}: '_' | @{syntax term}
wenzelm@27037
   296
    ;
wenzelm@42596
   297
    @{syntax_def insts}: (@{syntax inst} *)
wenzelm@55112
   298
  \<close>}
wenzelm@27037
   299
wenzelm@61662
   300
  Named instantiations are specified as pairs of assignments \<open>v = t\<close>, which
wenzelm@61662
   301
  refer to schematic variables in some theorem that is instantiated. Both type
wenzelm@61662
   302
  and terms instantiations are admitted, and distinguished by the usual syntax
wenzelm@61662
   303
  of variable names.
wenzelm@59853
   304
wenzelm@59853
   305
  @{rail \<open>
wenzelm@59853
   306
    @{syntax_def named_inst}: variable '=' (type | term)
wenzelm@59853
   307
    ;
wenzelm@59853
   308
    @{syntax_def named_insts}: (named_inst @'and' +)
wenzelm@59853
   309
    ;
wenzelm@63138
   310
    variable: @{syntax name} | @{syntax term_var} | @{syntax type_ident} | @{syntax type_var}
wenzelm@59853
   311
  \<close>}
wenzelm@59853
   312
wenzelm@61662
   313
  Type declarations and definitions usually refer to @{syntax typespec} on the
wenzelm@61662
   314
  left-hand side. This models basic type constructor application at the outer
wenzelm@61662
   315
  syntax level. Note that only plain postfix notation is available here, but
wenzelm@61662
   316
  no infixes.
wenzelm@27037
   317
wenzelm@55112
   318
  @{rail \<open>
wenzelm@42596
   319
    @{syntax_def typespec}:
wenzelm@63138
   320
      (() | @{syntax type_ident} | '(' ( @{syntax type_ident} + ',' ) ')') @{syntax name}
wenzelm@27037
   321
    ;
wenzelm@42705
   322
    @{syntax_def typespec_sorts}:
wenzelm@63138
   323
      (() | (@{syntax type_ident} ('::' @{syntax sort})?) |
wenzelm@63138
   324
        '(' ( (@{syntax type_ident} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
wenzelm@55112
   325
  \<close>}
wenzelm@58618
   326
\<close>
wenzelm@27037
   327
wenzelm@27037
   328
wenzelm@58618
   329
subsection \<open>Term patterns and declarations \label{sec:term-decls}\<close>
wenzelm@28754
   330
wenzelm@61662
   331
text \<open>
wenzelm@61662
   332
  Wherever explicit propositions (or term fragments) occur in a proof text,
wenzelm@61662
   333
  casual binding of schematic term variables may be given specified via
wenzelm@61663
   334
  patterns of the form ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>''. This works both for @{syntax
wenzelm@61662
   335
  term} and @{syntax prop}.
wenzelm@28754
   336
wenzelm@55112
   337
  @{rail \<open>
wenzelm@42705
   338
    @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')'
wenzelm@28754
   339
    ;
wenzelm@42705
   340
    @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')'
wenzelm@55112
   341
  \<close>}
wenzelm@28754
   342
wenzelm@61421
   343
  \<^medskip>
wenzelm@61662
   344
  Declarations of local variables \<open>x :: \<tau>\<close> and logical propositions \<open>a : \<phi>\<close>
wenzelm@61662
   345
  represent different views on the same principle of introducing a local
wenzelm@61662
   346
  scope. In practice, one may usually omit the typing of @{syntax vars} (due
wenzelm@61662
   347
  to type-inference), and the naming of propositions (due to implicit
wenzelm@61662
   348
  references of current facts). In any case, Isar proof elements usually admit
wenzelm@61662
   349
  to introduce multiple such items simultaneously.
wenzelm@28754
   350
wenzelm@55112
   351
  @{rail \<open>
wenzelm@63285
   352
    @{syntax_def vars}:
wenzelm@63285
   353
      (((@{syntax name} +) ('::' @{syntax type})? |
wenzelm@63285
   354
        @{syntax name} ('::' @{syntax type})? @{syntax mixfix}) + @'and')
wenzelm@28754
   355
    ;
wenzelm@42705
   356
    @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
wenzelm@61658
   357
    ;
wenzelm@61658
   358
    @{syntax_def props'}: (@{syntax prop} @{syntax prop_pat}? +)
wenzelm@55112
   359
  \<close>}
wenzelm@28754
   360
wenzelm@61662
   361
  The treatment of multiple declarations corresponds to the complementary
wenzelm@61662
   362
  focus of @{syntax vars} versus @{syntax props}. In ``\<open>x\<^sub>1 \<dots> x\<^sub>n :: \<tau>\<close>'' the
wenzelm@61662
   363
  typing refers to all variables, while in \<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> the naming refers to
wenzelm@61662
   364
  all propositions collectively. Isar language elements that refer to @{syntax
wenzelm@61662
   365
  vars} or @{syntax props} typically admit separate typings or namings via
wenzelm@61662
   366
  another level of iteration, with explicit @{keyword_ref "and"} separators;
wenzelm@61662
   367
  e.g.\ see @{command "fix"} and @{command "assume"} in
wenzelm@28754
   368
  \secref{sec:proof-context}.
wenzelm@61662
   369
\<close>
wenzelm@28754
   370
wenzelm@28754
   371
wenzelm@58618
   372
subsection \<open>Attributes and theorems \label{sec:syn-att}\<close>
wenzelm@27037
   373
wenzelm@61662
   374
text \<open>
wenzelm@61662
   375
  Attributes have their own ``semi-inner'' syntax, in the sense that input
wenzelm@61662
   376
  conforming to @{syntax args} below is parsed by the attribute a second time.
wenzelm@61662
   377
  The attribute argument specifications may be any sequence of atomic entities
wenzelm@61662
   378
  (identifiers, strings etc.), or properly bracketed argument lists. Below
wenzelm@61662
   379
  @{syntax atom} refers to any atomic entity, including any @{syntax keyword}
wenzelm@63138
   380
  conforming to @{syntax sym_ident}.
wenzelm@27037
   381
wenzelm@55112
   382
  @{rail \<open>
wenzelm@63138
   383
    @{syntax_def atom}: @{syntax name} | @{syntax type_ident} |
wenzelm@63138
   384
      @{syntax type_var} | @{syntax term_var} | @{syntax nat} | @{syntax float} |
wenzelm@55045
   385
      @{syntax keyword} | @{syntax cartouche}
wenzelm@27037
   386
    ;
wenzelm@42596
   387
    arg: @{syntax atom} | '(' @{syntax args} ')' | '[' @{syntax args} ']'
wenzelm@27037
   388
    ;
wenzelm@42596
   389
    @{syntax_def args}: arg *
wenzelm@27037
   390
    ;
wenzelm@62969
   391
    @{syntax_def attributes}: '[' (@{syntax name} @{syntax args} * ',') ']'
wenzelm@55112
   392
  \<close>}
wenzelm@27037
   393
wenzelm@61662
   394
  Theorem specifications come in several flavors: @{syntax axmdecl} and
wenzelm@61662
   395
  @{syntax thmdecl} usually refer to axioms, assumptions or results of goal
wenzelm@61662
   396
  statements, while @{syntax thmdef} collects lists of existing theorems.
wenzelm@62969
   397
  Existing theorems are given by @{syntax thm} and @{syntax thms}, the
wenzelm@61662
   398
  former requires an actual singleton result.
wenzelm@27037
   399
wenzelm@27037
   400
  There are three forms of theorem references:
wenzelm@60674
   401
wenzelm@61662
   402
    \<^enum> named facts \<open>a\<close>,
wenzelm@27037
   403
wenzelm@61662
   404
    \<^enum> selections from named facts \<open>a(i)\<close> or \<open>a(j - k)\<close>,
wenzelm@27037
   405
wenzelm@61662
   406
    \<^enum> literal fact propositions using token syntax @{syntax_ref altstring}
wenzelm@61662
   407
    \<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close> or @{syntax_ref cartouche}
wenzelm@61662
   408
    \<open>\<open>\<phi>\<close>\<close> (see also method @{method_ref fact}).
wenzelm@27037
   409
wenzelm@61662
   410
  Any kind of theorem specification may include lists of attributes both on
wenzelm@61662
   411
  the left and right hand sides; attributes are applied to any immediately
wenzelm@61662
   412
  preceding fact. If names are omitted, the theorems are not stored within the
wenzelm@61662
   413
  theorem database of the theory or proof context, but any given attributes
wenzelm@61662
   414
  are applied nonetheless.
wenzelm@27037
   415
wenzelm@61662
   416
  An extra pair of brackets around attributes (like ``\<open>[[simproc a]]\<close>'')
wenzelm@61662
   417
  abbreviates a theorem reference involving an internal dummy fact, which will
wenzelm@61662
   418
  be ignored later on. So only the effect of the attribute on the background
wenzelm@61662
   419
  context will persist. This form of in-place declarations is particularly
wenzelm@61662
   420
  useful with commands like @{command "declare"} and @{command "using"}.
wenzelm@27037
   421
wenzelm@55112
   422
  @{rail \<open>
wenzelm@42596
   423
    @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':'
wenzelm@42596
   424
    ;
wenzelm@60631
   425
    @{syntax_def thmbind}:
wenzelm@60631
   426
      @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
wenzelm@60631
   427
    ;
wenzelm@42596
   428
    @{syntax_def thmdecl}: thmbind ':'
wenzelm@27037
   429
    ;
wenzelm@42596
   430
    @{syntax_def thmdef}: thmbind '='
wenzelm@27037
   431
    ;
wenzelm@62969
   432
    @{syntax_def thm}:
wenzelm@62969
   433
      (@{syntax name} selection? | @{syntax altstring} | @{syntax cartouche})
wenzelm@56499
   434
        @{syntax attributes}? |
wenzelm@42596
   435
      '[' @{syntax attributes} ']'
wenzelm@27037
   436
    ;
wenzelm@62969
   437
    @{syntax_def thms}: @{syntax thm} +
wenzelm@27037
   438
    ;
wenzelm@42596
   439
    selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
wenzelm@55112
   440
  \<close>}
wenzelm@58618
   441
\<close>
wenzelm@27037
   442
wenzelm@60674
   443
wenzelm@63182
   444
subsection \<open>Structured specifications\<close>
wenzelm@63182
   445
wenzelm@63182
   446
text \<open>
wenzelm@63182
   447
  Structured specifications use propositions with explicit notation for the
wenzelm@63182
   448
  ``eigen-context'' to describe rule structure: \<open>\<And>x. A x \<Longrightarrow> \<dots> \<Longrightarrow> B x\<close> is
wenzelm@63182
   449
  expressed as \<^theory_text>\<open>B x if A x and \<dots> for x\<close>. It is also possible to use dummy
wenzelm@63182
   450
  terms ``\<open>_\<close>'' (underscore) to refer to locally fixed variables anonymously.
wenzelm@63182
   451
wenzelm@63182
   452
  Multiple specifications are delimited by ``\<open>|\<close>'' to emphasize separate
wenzelm@63182
   453
  cases: each with its own scope of inferred types for free variables.
wenzelm@63182
   454
wenzelm@63182
   455
wenzelm@63182
   456
  @{rail \<open>
wenzelm@63285
   457
    @{syntax_def for_fixes}: (@'for' @{syntax vars})?
wenzelm@63285
   458
    ;
wenzelm@63182
   459
    @{syntax_def multi_specs}: (@{syntax structured_spec} + '|')
wenzelm@63182
   460
    ;
wenzelm@63182
   461
    @{syntax_def structured_spec}:
wenzelm@63182
   462
      @{syntax thmdecl}? @{syntax prop} @{syntax spec_prems} @{syntax for_fixes}
wenzelm@63182
   463
    ;
wenzelm@63182
   464
    @{syntax_def spec_prems}: (@'if' ((@{syntax prop}+) + @'and'))?
wenzelm@63183
   465
    ;
wenzelm@63285
   466
    @{syntax_def specification}: @{syntax vars} @'where' @{syntax multi_specs}
wenzelm@63182
   467
  \<close>}
wenzelm@63182
   468
\<close>
wenzelm@63182
   469
wenzelm@63182
   470
wenzelm@60674
   471
section \<open>Diagnostic commands\<close>
wenzelm@60674
   472
wenzelm@60674
   473
text \<open>
wenzelm@60674
   474
  \begin{matharray}{rcl}
wenzelm@61493
   475
    @{command_def "print_theory"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   476
    @{command_def "print_definitions"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   477
    @{command_def "print_methods"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   478
    @{command_def "print_attributes"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   479
    @{command_def "print_theorems"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   480
    @{command_def "find_theorems"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   481
    @{command_def "find_consts"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   482
    @{command_def "thm_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   483
    @{command_def "unused_thms"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   484
    @{command_def "print_facts"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   485
    @{command_def "print_term_bindings"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@60674
   486
  \end{matharray}
wenzelm@60674
   487
wenzelm@60674
   488
  @{rail \<open>
wenzelm@60674
   489
    (@@{command print_theory} |
wenzelm@61252
   490
      @@{command print_definitions} |
wenzelm@60674
   491
      @@{command print_methods} |
wenzelm@60674
   492
      @@{command print_attributes} |
wenzelm@60674
   493
      @@{command print_theorems} |
wenzelm@60674
   494
      @@{command print_facts}) ('!'?)
wenzelm@60674
   495
    ;
wenzelm@60674
   496
    @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*)
wenzelm@60674
   497
    ;
wenzelm@62969
   498
    thm_criterion: ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
wenzelm@60674
   499
      'solves' | 'simp' ':' @{syntax term} | @{syntax term})
wenzelm@60674
   500
    ;
wenzelm@60674
   501
    @@{command find_consts} (const_criterion*)
wenzelm@60674
   502
    ;
wenzelm@60674
   503
    const_criterion: ('-'?)
wenzelm@62969
   504
      ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
wenzelm@60674
   505
    ;
wenzelm@60674
   506
    @@{command thm_deps} @{syntax thmrefs}
wenzelm@60674
   507
    ;
wenzelm@60674
   508
    @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
wenzelm@60674
   509
  \<close>}
wenzelm@60674
   510
wenzelm@61662
   511
  These commands print certain parts of the theory and proof context. Note
wenzelm@61662
   512
  that there are some further ones available, such as for the set of rules
wenzelm@61662
   513
  declared for simplifications.
wenzelm@60674
   514
wenzelm@61439
   515
  \<^descr> @{command "print_theory"} prints the main logical content of the
wenzelm@61493
   516
  background theory; the ``\<open>!\<close>'' option indicates extra verbosity.
wenzelm@60674
   517
wenzelm@61439
   518
  \<^descr> @{command "print_definitions"} prints dependencies of definitional
wenzelm@61252
   519
  specifications within the background theory, which may be constants
wenzelm@62172
   520
  (\secref{sec:term-definitions}, \secref{sec:overloading}) or types
wenzelm@62172
   521
  (\secref{sec:types-pure}, \secref{sec:hol-typedef}); the ``\<open>!\<close>'' option
wenzelm@62172
   522
  indicates extra verbosity.
wenzelm@61252
   523
wenzelm@61439
   524
  \<^descr> @{command "print_methods"} prints all proof methods available in the
wenzelm@61662
   525
  current theory context; the ``\<open>!\<close>'' option indicates extra verbosity.
wenzelm@60674
   526
wenzelm@61439
   527
  \<^descr> @{command "print_attributes"} prints all attributes available in the
wenzelm@61662
   528
  current theory context; the ``\<open>!\<close>'' option indicates extra verbosity.
wenzelm@60674
   529
wenzelm@61439
   530
  \<^descr> @{command "print_theorems"} prints theorems of the background theory
wenzelm@61662
   531
  resulting from the last command; the ``\<open>!\<close>'' option indicates extra
wenzelm@61662
   532
  verbosity.
wenzelm@60674
   533
wenzelm@61662
   534
  \<^descr> @{command "print_facts"} prints all local facts of the current context,
wenzelm@61662
   535
  both named and unnamed ones; the ``\<open>!\<close>'' option indicates extra verbosity.
wenzelm@60674
   536
wenzelm@61662
   537
  \<^descr> @{command "print_term_bindings"} prints all term bindings that are present
wenzelm@61662
   538
  in the context.
wenzelm@60674
   539
wenzelm@61662
   540
  \<^descr> @{command "find_theorems"}~\<open>criteria\<close> retrieves facts from the theory or
wenzelm@61662
   541
  proof context matching all of given search criteria. The criterion \<open>name: p\<close>
wenzelm@61662
   542
  selects all theorems whose fully qualified name matches pattern \<open>p\<close>, which
wenzelm@61662
   543
  may contain ``\<open>*\<close>'' wildcards. The criteria \<open>intro\<close>, \<open>elim\<close>, and \<open>dest\<close>
wenzelm@61662
   544
  select theorems that match the current goal as introduction, elimination or
wenzelm@61662
   545
  destruction rules, respectively. The criterion \<open>solves\<close> returns all rules
wenzelm@61662
   546
  that would directly solve the current goal. The criterion \<open>simp: t\<close> selects
wenzelm@61662
   547
  all rewrite rules whose left-hand side matches the given term. The criterion
wenzelm@61662
   548
  term \<open>t\<close> selects all theorems that contain the pattern \<open>t\<close> -- as usual,
wenzelm@61662
   549
  patterns may contain occurrences of the dummy ``\<open>_\<close>'', schematic variables,
wenzelm@61662
   550
  and type constraints.
wenzelm@60674
   551
wenzelm@61662
   552
  Criteria can be preceded by ``\<open>-\<close>'' to select theorems that do \<^emph>\<open>not\<close> match.
wenzelm@61662
   553
  Note that giving the empty list of criteria yields \<^emph>\<open>all\<close> currently known
wenzelm@61662
   554
  facts. An optional limit for the number of printed facts may be given; the
wenzelm@61662
   555
  default is 40. By default, duplicates are removed from the search result.
wenzelm@61662
   556
  Use \<open>with_dups\<close> to display duplicates.
wenzelm@60674
   557
wenzelm@61662
   558
  \<^descr> @{command "find_consts"}~\<open>criteria\<close> prints all constants whose type meets
wenzelm@61662
   559
  all of the given criteria. The criterion \<open>strict: ty\<close> is met by any type
wenzelm@61662
   560
  that matches the type pattern \<open>ty\<close>. Patterns may contain both the dummy type
wenzelm@61662
   561
  ``\<open>_\<close>'' and sort constraints. The criterion \<open>ty\<close> is similar, but it also
wenzelm@61662
   562
  matches against subtypes. The criterion \<open>name: p\<close> and the prefix ``\<open>-\<close>''
wenzelm@61662
   563
  function as described for @{command "find_theorems"}.
wenzelm@60674
   564
wenzelm@61662
   565
  \<^descr> @{command "thm_deps"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> visualizes dependencies of facts, using
wenzelm@61662
   566
  Isabelle's graph browser tool (see also @{cite "isabelle-system"}).
wenzelm@60674
   567
wenzelm@61662
   568
  \<^descr> @{command "unused_thms"}~\<open>A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n\<close> displays all theorems
wenzelm@61662
   569
  that are proved in theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close> or their parents but not in \<open>A\<^sub>1 \<dots>
wenzelm@61662
   570
  A\<^sub>m\<close> or their parents and that are never used. If \<open>n\<close> is \<open>0\<close>, the end of the
wenzelm@61662
   571
  range of theories defaults to the current theory. If no range is specified,
wenzelm@60674
   572
  only the unused theorems in the current theory are displayed.
wenzelm@60674
   573
\<close>
wenzelm@60674
   574
wenzelm@27037
   575
end