1.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:54:51 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:56:23 2008 +0100
     1.3 @@ -462,6 +462,94 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +subsection {* The Pure grammar *}
     1.8 +
     1.9 +text {*
    1.10 +  \begin{figure}[htb]\small
    1.11 +  \begin{center}
    1.12 +  \begin{tabular}{rclc}
    1.13 +
    1.14 +    @{text any} & = & @{text "prop  |  logic"} \\\\
    1.15 +    % FIXME
    1.16 +
    1.17 +  \end{tabular}
    1.18 +  \end{center}
    1.19 +  \caption{The Pure grammar}\label{fig:pure-grammar}
    1.20 +  \end{figure}
    1.21 +
    1.22 +  The priority grammar of the @{text "Pure"} theory is defined in
    1.23 +  \figref{fig:pure-grammar}.  The following nonterminals are
    1.24 +  introduced:
    1.25 +
    1.26 +  \begin{description}
    1.27 +
    1.28 +  \item @{text "any"} denotes any term.
    1.29 +
    1.30 +  \item @{text "prop"} denotes meta-level propositions, which are
    1.31 +  terms of type @{typ prop}.  The syntax of such formulae of the
    1.32 +  meta-logic is carefully distinguished from usual conventions for
    1.33 +  object-logics.  In particular, plain @{text "\<lambda>"}-term
    1.34 +  notation is \emph{not} recognized as @{text "prop"}.
    1.35 +
    1.36 +  \item @{text aprop} denotes atomic propositions, which are embedded
    1.37 +  into regular @{typ prop} by means of an explicit @{text "PROP"}
    1.38 +  token.
    1.39 +
    1.40 +  Terms of type @{typ prop} with non-constant head, e.g.\ a plain
    1.41 +  variable, are printed in this form.  Constants that yield type @{typ
    1.42 +  prop} are expected to provide their own concrete syntax; otherwise
    1.43 +  the printed version will appear like @{typ logic} and cannot be
    1.44 +  parsed again as @{typ prop}.
    1.45 +
    1.46 +  \item @{text logic} denotes arbitrary terms of a logical type,
    1.47 +  excluding type @{typ prop}.  This is the main syntactic category of
    1.48 +  object-logic entities, covering plain @{text \<lambda>}-term notation
    1.49 +  (variables, abstraction, application), plus anything defined by the
    1.50 +  user.
    1.51 +
    1.52 +  When specifying notation for logical entities, all logical types
    1.53 +  (excluding @{typ prop}) are \emph{collapsed} to this single category
    1.54 +  of @{typ logic}.
    1.55 +
    1.56 +  \item @{text idt} denotes identifiers, possibly constrained by
    1.57 +  types.
    1.58 +
    1.59 +  \item @{text idts} denotes a sequence of @{text idt}.  This is the
    1.60 +  most basic category for variables in iterated binders, such as
    1.61 +  @{text "\<lambda>"} or @{text "\<And>"}.
    1.62 +
    1.63 +  \item @{text pttrn} and @{text pttrns} denote patterns for
    1.64 +  abstraction, cases bindings etc.  In Pure, these categories start as
    1.65 +  a merely copy of @{text idt} and @{text idts}, respectively.
    1.66 +  Object-logics may add additional productions for binding forms.
    1.67 +
    1.68 +  \item @{text type} denotes types of the meta-logic.
    1.69 +
    1.70 +  \item @{text sort} denotes meta-level sorts.
    1.71 +
    1.72 +  \end{description}
    1.73 +
    1.74 +  \begin{warn}
    1.75 +  In @{text idts}, note that @{text "x :: nat y"} is parsed as @{text
    1.76 +  "x :: (nat y)"}, treating @{text y} like a type constructor applied
    1.77 +  to @{text nat}.  To avoid this interpretation, write @{text "(x ::
    1.78 +  nat) y"} with explicit parentheses.
    1.79 +
    1.80 +  Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x ::
    1.81 +  (nat y :: nat)"}.  The correct form is @{text "(x :: nat) (y ::
    1.82 +  nat)"}, or @{text "(x :: nat) y :: nat"} if @{text y} is last in the
    1.83 +  sequence of identifiers.
    1.84 +  \end{warn}
    1.85 +
    1.86 +  \begin{warn}
    1.87 +  Type constraints for terms bind very weakly.  For example, @{text "x
    1.88 +  < y :: nat"} is normally parsed as @{text "(x < y) :: nat"}, unless
    1.89 +  @{text "<"} has a very low priority, in which case the input is
    1.90 +  likely to be ambiguous.  The correct form is @{text "x < (y :: nat)"}.
    1.91 +  \end{warn}
    1.92 +*}
    1.93 +
    1.94 +
    1.95  section {* Syntax and translations \label{sec:syn-trans} *}
    1.96  
    1.97  text {*