src/Doc/IsarRef/Outer_Syntax.thy
author wenzelm
Sun, 18 Aug 2013 13:25:31 +0200
changeset 53059 f4811f3628dc
parent 53015 a1119cf551e8
child 55033 8e8243975860
permissions -rw-r--r--
updated identifier syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     1
theory Outer_Syntax
42651
e3fdb7c96be5 formal Base theory;
wenzelm
parents: 42596
diff changeset
     2
imports Base Main
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     3
begin
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     4
47114
7c9e31ffcd9e updated theory header syntax and related details;
wenzelm
parents: 46282
diff changeset
     5
chapter {* Outer syntax --- the theory language \label{ch:outer-syntax} *}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     6
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     7
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     8
  The rather generic framework of Isabelle/Isar syntax emerges from
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     9
  three main syntactic categories: \emph{commands} of the top-level
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    10
  Isar engine (covering theory and proof elements), \emph{methods} for
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    11
  general goal refinements (analogous to traditional ``tactics''), and
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    12
  \emph{attributes} for operations on facts (within a certain
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    13
  context).  Subsequently we give a reference of basic syntactic
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    14
  entities underlying Isabelle/Isar syntax in a bottom-up manner.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    15
  Concrete theory and proof language elements will be introduced later
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    16
  on.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    17
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    18
  \medskip In order to get started with writing well-formed
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    19
  Isabelle/Isar documents, the most important aspect to be noted is
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    20
  the difference of \emph{inner} versus \emph{outer} syntax.  Inner
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    21
  syntax is that of Isabelle types and terms of the logic, while outer
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    22
  syntax is that of Isabelle/Isar theory sources (specifications and
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    23
  proofs).  As a general rule, inner syntax entities may occur only as
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    24
  \emph{atomic entities} within outer syntax.  For example, the string
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    25
  @{verbatim "\"x + y\""} and identifier @{verbatim z} are legal term
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    26
  specifications within a theory, while @{verbatim "x + y"} without
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    27
  quotes is not.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    28
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    29
  Printed theory documents usually omit quotes to gain readability
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    30
  (this is a matter of {\LaTeX} macro setup, say via @{verbatim
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    31
  "\\isabellestyle"}, see also \cite{isabelle-sys}).  Experienced
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    32
  users of Isabelle/Isar may easily reconstruct the lost technical
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    33
  information, while mere readers need not care about quotes at all.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    34
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    35
  \medskip Isabelle/Isar input may contain any number of input
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    36
  termination characters ``@{verbatim ";"}'' (semicolon) to separate
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    37
  commands explicitly.  This is particularly useful in interactive
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    38
  shell sessions to make clear where the current command is intended
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    39
  to end.  Otherwise, the interpreter loop will continue to issue a
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    40
  secondary prompt ``@{verbatim "#"}'' until an end-of-command is
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    41
  clearly recognized from the input syntax, e.g.\ encounter of the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    42
  next command keyword.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    43
51058
98c48d023136 some updates concerning Proof General;
wenzelm
parents: 50213
diff changeset
    44
  More advanced interfaces such as Isabelle/jEdit \cite{Wenzel:2012}
98c48d023136 some updates concerning Proof General;
wenzelm
parents: 50213
diff changeset
    45
  and Proof~General \cite{proofgeneral} do not require explicit
51062
wenzelm
parents: 51058
diff changeset
    46
  semicolons: command spans are determined by inspecting the content
wenzelm
parents: 51058
diff changeset
    47
  of the editor buffer.  In the printed presentation of Isabelle/Isar
wenzelm
parents: 51058
diff changeset
    48
  documents semicolons are omitted altogether for readability.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    49
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    50
  \begin{warn}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    51
    Proof~General requires certain syntax classification tables in
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    52
    order to achieve properly synchronized interaction with the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    53
    Isabelle/Isar process.  These tables need to be consistent with
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    54
    the Isabelle version and particular logic image to be used in a
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    55
    running session (common object-logics may well change the outer
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    56
    syntax).  The standard setup should work correctly with any of the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    57
    ``official'' logic images derived from Isabelle/HOL (including
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    58
    HOLCF etc.).  Users of alternative logics may need to tell
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    59
    Proof~General explicitly, e.g.\ by giving an option @{verbatim "-k ZF"}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    60
    (in conjunction with @{verbatim "-l ZF"}, to specify the default
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    61
    logic image).  Note that option @{verbatim "-L"} does both
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    62
    of this at the same time.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    63
  \end{warn}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    64
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    65
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    66
50213
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    67
section {* Commands *}
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    68
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    69
text {*
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    70
  \begin{matharray}{rcl}
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    71
    @{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    72
    @{command_def "help"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    73
  \end{matharray}
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    74
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    75
  @{rail "
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    76
    @@{command help} (@{syntax name} * )
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    77
  "}
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    78
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    79
  \begin{description}
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    80
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    81
  \item @{command "print_commands"} prints all outer syntax keywords
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    82
  and commands.
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    83
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    84
  \item @{command "help"}~@{text "pats"} retrieves outer syntax
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    85
  commands according to the specified name patterns.
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    86
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    87
  \end{description}
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    88
*}
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    89
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    90
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    91
subsubsection {* Examples *}
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    92
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    93
text {* Some common diagnostic commands are retrieved like this
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    94
  (according to usual naming conventions): *}
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    95
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    96
help "print"
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    97
help "find"
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    98
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    99
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28762
diff changeset
   100
section {* Lexical matters \label{sec:outer-lex} *}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   101
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   102
text {* The outer lexical syntax consists of three main categories of
28776
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   103
  syntax tokens:
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   104
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   105
  \begin{enumerate}
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   106
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   107
  \item \emph{major keywords} --- the command names that are available
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   108
  in the present logic session;
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   109
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   110
  \item \emph{minor keywords} --- additional literal tokens required
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   111
  by the syntax of commands;
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   112
28776
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   113
  \item \emph{named tokens} --- various categories of identifiers etc.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   114
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   115
  \end{enumerate}
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   116
28776
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   117
  Major keywords and minor keywords are guaranteed to be disjoint.
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   118
  This helps user-interfaces to determine the overall structure of a
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   119
  theory text, without knowing the full details of command syntax.
28776
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   120
  Internally, there is some additional information about the kind of
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   121
  major keywords, which approximates the command type (theory command,
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   122
  proof command etc.).
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   123
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   124
  Keywords override named tokens.  For example, the presence of a
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   125
  command called @{verbatim term} inhibits the identifier @{verbatim
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   126
  term}, but the string @{verbatim "\"term\""} can be used instead.
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   127
  By convention, the outer syntax always allows quoted strings in
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   128
  addition to identifiers, wherever a named entity is expected.
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   129
28776
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   130
  When tokenizing a given input sequence, the lexer repeatedly takes
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   131
  the longest prefix of the input that forms a valid token.  Spaces,
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   132
  tabs, newlines and formfeeds between tokens serve as explicit
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   133
  separators.
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   134
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   135
  \medskip The categories for named tokens are defined once and for
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   136
  all as follows.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   137
28776
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   138
  \begin{center}
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   139
  \begin{supertabular}{rcl}
53059
f4811f3628dc updated identifier syntax;
wenzelm
parents: 53015
diff changeset
   140
    @{syntax_def ident} & = & @{text "letter (subscript\<^sup>? quasiletter)\<^sup>*"} \\
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   141
    @{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   142
    @{syntax_def symident} & = & @{text "sym\<^sup>+  |  "}@{verbatim "\\"}@{verbatim "<"}@{text ident}@{verbatim ">"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   143
    @{syntax_def nat} & = & @{text "digit\<^sup>+"} \\
40290
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 35841
diff changeset
   144
    @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   145
    @{syntax_def var} & = & @{verbatim "?"}@{text "ident  |  "}@{verbatim "?"}@{text ident}@{verbatim "."}@{text nat} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   146
    @{syntax_def typefree} & = & @{verbatim "'"}@{text ident} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   147
    @{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree  |  "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   148
    @{syntax_def string} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   149
    @{syntax_def altstring} & = & @{verbatim "`"} @{text "\<dots>"} @{verbatim "`"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   150
    @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*"}@{verbatim "}"} \\[1ex]
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   151
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   152
    @{text letter} & = & @{text "latin  |  "}@{verbatim "\\"}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text "  |  "}@{verbatim "\\"}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text "  |  greek  |"} \\
53059
f4811f3628dc updated identifier syntax;
wenzelm
parents: 53015
diff changeset
   153
    @{text subscript} & = & @{verbatim "\<^sub>"} \\
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   154
    @{text quasiletter} & = & @{text "letter  |  digit  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "'"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   155
    @{text latin} & = & @{verbatim a}@{text "  | \<dots> |  "}@{verbatim z}@{text "  |  "}@{verbatim A}@{text "  |  \<dots> |  "}@{verbatim Z} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   156
    @{text digit} & = & @{verbatim "0"}@{text "  |  \<dots> |  "}@{verbatim "9"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   157
    @{text sym} & = & @{verbatim "!"}@{text "  |  "}@{verbatim "#"}@{text "  |  "}@{verbatim "$"}@{text "  |  "}@{verbatim "%"}@{text "  |  "}@{verbatim "&"}@{text "  |  "}@{verbatim "*"}@{text "  |  "}@{verbatim "+"}@{text "  |  "}@{verbatim "-"}@{text "  |  "}@{verbatim "/"}@{text "  |"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   158
    & & @{verbatim "<"}@{text "  |  "}@{verbatim "="}@{text "  |  "}@{verbatim ">"}@{text "  |  "}@{verbatim "?"}@{text "  |  "}@{verbatim "@"}@{text "  |  "}@{verbatim "^"}@{text "  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "|"}@{text "  |  "}@{verbatim "~"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   159
    @{text greek} & = & @{verbatim "\<alpha>"}@{text "  |  "}@{verbatim "\<beta>"}@{text "  |  "}@{verbatim "\<gamma>"}@{text "  |  "}@{verbatim "\<delta>"}@{text "  |"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   160
          &   & @{verbatim "\<epsilon>"}@{text "  |  "}@{verbatim "\<zeta>"}@{text "  |  "}@{verbatim "\<eta>"}@{text "  |  "}@{verbatim "\<theta>"}@{text "  |"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   161
          &   & @{verbatim "\<iota>"}@{text "  |  "}@{verbatim "\<kappa>"}@{text "  |  "}@{verbatim "\<mu>"}@{text "  |  "}@{verbatim "\<nu>"}@{text "  |"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   162
          &   & @{verbatim "\<xi>"}@{text "  |  "}@{verbatim "\<pi>"}@{text "  |  "}@{verbatim "\<rho>"}@{text "  |  "}@{verbatim "\<sigma>"}@{text "  |  "}@{verbatim "\<tau>"}@{text "  |"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   163
          &   & @{verbatim "\<upsilon>"}@{text "  |  "}@{verbatim "\<phi>"}@{text "  |  "}@{verbatim "\<chi>"}@{text "  |  "}@{verbatim "\<psi>"}@{text "  |"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   164
          &   & @{verbatim "\<omega>"}@{text "  |  "}@{verbatim "\<Gamma>"}@{text "  |  "}@{verbatim "\<Delta>"}@{text "  |  "}@{verbatim "\<Theta>"}@{text "  |"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   165
          &   & @{verbatim "\<Lambda>"}@{text "  |  "}@{verbatim "\<Xi>"}@{text "  |  "}@{verbatim "\<Pi>"}@{text "  |  "}@{verbatim "\<Sigma>"}@{text "  |"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   166
          &   & @{verbatim "\<Upsilon>"}@{text "  |  "}@{verbatim "\<Phi>"}@{text "  |  "}@{verbatim "\<Psi>"}@{text "  |  "}@{verbatim "\<Omega>"} \\
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   167
  \end{supertabular}
28776
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   168
  \end{center}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   169
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   170
  A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown,
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   171
  which is internally a pair of base name and index (ML type @{ML_type
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   172
  indexname}).  These components are either separated by a dot as in
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   173
  @{text "?x.1"} or @{text "?x7.3"} or run together as in @{text
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   174
  "?x1"}.  The latter form is possible if the base name does not end
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   175
  with digits.  If the index is 0, it may be dropped altogether:
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   176
  @{text "?x"} and @{text "?x0"} and @{text "?x.0"} all refer to the
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   177
  same unknown, with basename @{text "x"} and index 0.
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   178
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   179
  The syntax of @{syntax_ref string} admits any characters, including
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   180
  newlines; ``@{verbatim "\""}'' (double-quote) and ``@{verbatim
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   181
  "\\"}'' (backslash) need to be escaped by a backslash; arbitrary
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   182
  character codes may be specified as ``@{verbatim "\\"}@{text ddd}'',
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   183
  with three decimal digits.  Alternative strings according to
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   184
  @{syntax_ref altstring} are analogous, using single back-quotes
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   185
  instead.
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   186
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   187
  The body of @{syntax_ref verbatim} may consist of any text not
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   188
  containing ``@{verbatim "*"}@{verbatim "}"}''; this allows
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   189
  convenient inclusion of quotes without further escapes.  There is no
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   190
  way to escape ``@{verbatim "*"}@{verbatim "}"}''.  If the quoted
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   191
  text is {\LaTeX} source, one may usually add some blank or comment
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   192
  to avoid the critical character sequence.
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   193
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   194
  Source comments take the form @{verbatim "(*"}~@{text
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   195
  "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   196
  might prevent this.  Note that this form indicates source comments
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   197
  only, which are stripped after lexical analysis of the input.  The
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   198
  Isar syntax also provides proper \emph{document comments} that are
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   199
  considered as part of the text (see \secref{sec:comments}).
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   200
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   201
  Common mathematical symbols such as @{text \<forall>} are represented in
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   202
  Isabelle as @{verbatim \<forall>}.  There are infinitely many Isabelle
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   203
  symbols like this, although proper presentation is left to front-end
47822
34b44d28fc4b some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
wenzelm
parents: 47114
diff changeset
   204
  tools such as {\LaTeX}, Proof~General, or Isabelle/jEdit.  A list of
34b44d28fc4b some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
wenzelm
parents: 47114
diff changeset
   205
  predefined Isabelle symbols that work well with these tools is given
34b44d28fc4b some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
wenzelm
parents: 47114
diff changeset
   206
  in \appref{app:symbols}.  Note that @{verbatim "\<lambda>"} does not belong
34b44d28fc4b some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
wenzelm
parents: 47114
diff changeset
   207
  to the @{text letter} category, since it is already used differently
34b44d28fc4b some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
wenzelm
parents: 47114
diff changeset
   208
  in the Pure term language.  *}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   209
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   210
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   211
section {* Common syntax entities *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   212
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   213
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   214
  We now introduce several basic syntactic entities, such as names,
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   215
  terms, and theorem specifications, which are factored out of the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   216
  actual Isar language elements to be described later.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   217
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   218
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   219
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   220
subsection {* Names *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   221
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   222
text {* Entity @{syntax name} usually refers to any name of types,
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   223
  constants, theorems etc.\ that are to be \emph{declared} or
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   224
  \emph{defined} (so qualified identifiers are excluded here).  Quoted
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   225
  strings provide an escape for non-identifier names or those ruled
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   226
  out by outer syntax keywords (e.g.\ quoted @{verbatim "\"let\""}).
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   227
  Already existing objects are usually referenced by @{syntax
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   228
  nameref}.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   229
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   230
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   231
    @{syntax_def name}: @{syntax ident} | @{syntax symident} |
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   232
      @{syntax string} | @{syntax nat}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   233
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   234
    @{syntax_def parname}: '(' @{syntax name} ')'
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   235
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   236
    @{syntax_def nameref}: @{syntax name} | @{syntax longident}
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   237
  "}
40296
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   238
*}
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   239
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   240
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   241
subsection {* Numbers *}
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   242
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   243
text {* The outer lexical syntax (\secref{sec:outer-lex}) admits
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   244
  natural numbers and floating point numbers.  These are combined as
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   245
  @{syntax int} and @{syntax real} as follows.
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   246
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   247
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   248
    @{syntax_def int}: @{syntax nat} | '-' @{syntax nat}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   249
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   250
    @{syntax_def real}: @{syntax float} | @{syntax int}
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   251
  "}
40296
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   252
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   253
  Note that there is an overlap with the category @{syntax name},
40296
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   254
  which also includes @{syntax nat}.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   255
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   256
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   257
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   258
subsection {* Comments \label{sec:comments} *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   259
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   260
text {* Large chunks of plain @{syntax text} are usually given
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   261
  @{syntax verbatim}, i.e.\ enclosed in @{verbatim "{"}@{verbatim
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   262
  "*"}~@{text "\<dots>"}~@{verbatim "*"}@{verbatim "}"}.  For convenience,
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   263
  any of the smaller text units conforming to @{syntax nameref} are
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   264
  admitted as well.  A marginal @{syntax comment} is of the form
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   265
  @{verbatim "--"}~@{syntax text}.  Any number of these may occur
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   266
  within Isabelle/Isar commands.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   267
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   268
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   269
    @{syntax_def text}: @{syntax verbatim} | @{syntax nameref}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   270
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   271
    @{syntax_def comment}: '--' @{syntax text}
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   272
  "}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   273
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   274
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   275
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   276
subsection {* Type classes, sorts and arities *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   277
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   278
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   279
  Classes are specified by plain names.  Sorts have a very simple
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   280
  inner syntax, which is either a single class name @{text c} or a
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   281
  list @{text "{c\<^sub>1, \<dots>, c\<^sub>n}"} referring to the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   282
  intersection of these classes.  The syntax of type arities is given
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   283
  directly at the outer level.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   284
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   285
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   286
    @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax nameref} + ','))?
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   287
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   288
    @{syntax_def sort}: @{syntax nameref}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   289
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   290
    @{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort}
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   291
  "}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   292
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   293
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   294
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   295
subsection {* Types and terms \label{sec:types-terms} *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   296
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   297
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   298
  The actual inner Isabelle syntax, that of types and terms of the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   299
  logic, is far too sophisticated in order to be modelled explicitly
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   300
  at the outer theory level.  Basically, any such entity has to be
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   301
  quoted to turn it into a single token (the parsing and type-checking
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   302
  is performed internally later).  For convenience, a slightly more
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   303
  liberal convention is adopted: quotes may be omitted for any type or
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   304
  term that is already atomic at the outer level.  For example, one
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   305
  may just write @{verbatim x} instead of quoted @{verbatim "\"x\""}.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   306
  Note that symbolic identifiers (e.g.\ @{verbatim "++"} or @{text
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   307
  "\<forall>"} are available as well, provided these have not been superseded
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   308
  by commands or other keywords already (such as @{verbatim "="} or
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   309
  @{verbatim "+"}).
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   310
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   311
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   312
    @{syntax_def type}: @{syntax nameref} | @{syntax typefree} |
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   313
      @{syntax typevar}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   314
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   315
    @{syntax_def term}: @{syntax nameref} | @{syntax var}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   316
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   317
    @{syntax_def prop}: @{syntax term}
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   318
  "}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   319
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   320
  Positional instantiations are indicated by giving a sequence of
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   321
  terms, or the placeholder ``@{text _}'' (underscore), which means to
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   322
  skip a position.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   323
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   324
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   325
    @{syntax_def inst}: '_' | @{syntax term}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   326
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   327
    @{syntax_def insts}: (@{syntax inst} *)
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   328
  "}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   329
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   330
  Type declarations and definitions usually refer to @{syntax
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   331
  typespec} on the left-hand side.  This models basic type constructor
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   332
  application at the outer syntax level.  Note that only plain postfix
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   333
  notation is available here, but no infixes.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   334
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   335
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   336
    @{syntax_def typespec}:
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   337
      (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   338
    ;
42705
528a2ba8fa74 tuned some syntax names;
wenzelm
parents: 42651
diff changeset
   339
    @{syntax_def typespec_sorts}:
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   340
      (() | (@{syntax typefree} ('::' @{syntax sort})?) |
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   341
        '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   342
  "}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   343
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   344
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   345
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   346
subsection {* Term patterns and declarations \label{sec:term-decls} *}
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   347
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   348
text {* Wherever explicit propositions (or term fragments) occur in a
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   349
  proof text, casual binding of schematic term variables may be given
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   350
  specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}''.
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   351
  This works both for @{syntax term} and @{syntax prop}.
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   352
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   353
  @{rail "
42705
528a2ba8fa74 tuned some syntax names;
wenzelm
parents: 42651
diff changeset
   354
    @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')'
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   355
    ;
42705
528a2ba8fa74 tuned some syntax names;
wenzelm
parents: 42651
diff changeset
   356
    @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')'
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   357
  "}
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   358
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   359
  \medskip Declarations of local variables @{text "x :: \<tau>"} and
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   360
  logical propositions @{text "a : \<phi>"} represent different views on
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   361
  the same principle of introducing a local scope.  In practice, one
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   362
  may usually omit the typing of @{syntax vars} (due to
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   363
  type-inference), and the naming of propositions (due to implicit
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   364
  references of current facts).  In any case, Isar proof elements
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   365
  usually admit to introduce multiple such items simultaneously.
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   366
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   367
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   368
    @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   369
    ;
42705
528a2ba8fa74 tuned some syntax names;
wenzelm
parents: 42651
diff changeset
   370
    @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   371
  "}
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   372
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   373
  The treatment of multiple declarations corresponds to the
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   374
  complementary focus of @{syntax vars} versus @{syntax props}.  In
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   375
  ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}'' the typing refers to all variables, while
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   376
  in @{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} the naming refers to all propositions
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   377
  collectively.  Isar language elements that refer to @{syntax vars}
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   378
  or @{syntax props} typically admit separate typings or namings via
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   379
  another level of iteration, with explicit @{keyword_ref "and"}
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   380
  separators; e.g.\ see @{command "fix"} and @{command "assume"} in
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   381
  \secref{sec:proof-context}.
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   382
*}
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   383
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   384
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   385
subsection {* Attributes and theorems \label{sec:syn-att} *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   386
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   387
text {* Attributes have their own ``semi-inner'' syntax, in the sense
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   388
  that input conforming to @{syntax args} below is parsed by the
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   389
  attribute a second time.  The attribute argument specifications may
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   390
  be any sequence of atomic entities (identifiers, strings etc.), or
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   391
  properly bracketed argument lists.  Below @{syntax atom} refers to
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   392
  any atomic entity, including any @{syntax keyword} conforming to
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   393
  @{syntax symident}.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   394
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   395
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   396
    @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} |
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   397
      @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   398
      @{syntax keyword}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   399
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   400
    arg: @{syntax atom} | '(' @{syntax args} ')' | '[' @{syntax args} ']'
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   401
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   402
    @{syntax_def args}: arg *
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   403
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   404
    @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']'
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   405
  "}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   406
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   407
  Theorem specifications come in several flavors: @{syntax axmdecl}
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   408
  and @{syntax thmdecl} usually refer to axioms, assumptions or
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   409
  results of goal statements, while @{syntax thmdef} collects lists of
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   410
  existing theorems.  Existing theorems are given by @{syntax thmref}
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   411
  and @{syntax thmrefs}, the former requires an actual singleton
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   412
  result.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   413
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   414
  There are three forms of theorem references:
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   415
  \begin{enumerate}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   416
  
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   417
  \item named facts @{text "a"},
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   418
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   419
  \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   420
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   421
  \item literal fact propositions using @{syntax_ref altstring} syntax
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   422
  @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   423
  @{method_ref fact}).
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   424
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   425
  \end{enumerate}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   426
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   427
  Any kind of theorem specification may include lists of attributes
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   428
  both on the left and right hand sides; attributes are applied to any
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   429
  immediately preceding fact.  If names are omitted, the theorems are
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   430
  not stored within the theorem database of the theory or proof
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   431
  context, but any given attributes are applied nonetheless.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   432
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   433
  An extra pair of brackets around attributes (like ``@{text
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   434
  "[[simproc a]]"}'') abbreviates a theorem reference involving an
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   435
  internal dummy fact, which will be ignored later on.  So only the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   436
  effect of the attribute on the background context will persist.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   437
  This form of in-place declarations is particularly useful with
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   438
  commands like @{command "declare"} and @{command "using"}.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   439
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   440
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   441
    @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':'
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   442
    ;
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   443
    @{syntax_def thmdecl}: thmbind ':'
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   444
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   445
    @{syntax_def thmdef}: thmbind '='
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   446
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   447
    @{syntax_def thmref}:
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   448
      (@{syntax nameref} selection? | @{syntax altstring}) @{syntax attributes}? |
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   449
      '[' @{syntax attributes} ']'
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   450
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   451
    @{syntax_def thmrefs}: @{syntax thmref} +
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   452
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   453
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   454
    thmbind: @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   455
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   456
    selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   457
  "}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   458
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   459
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   460
end