1.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:57:20 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:57:50 2008 +0100
     1.3 @@ -473,55 +473,65 @@
     1.4  subsection {* The Pure grammar *}
     1.5  
     1.6  text {*
     1.7 -  \begin{figure}[htb]\small
     1.8 +  The priority grammar of the @{text "Pure"} theory is defined as follows:
     1.9 +
    1.10    \begin{center}
    1.11 -  \begin{tabular}{rclc}
    1.12 +  \begin{supertabular}{rclr}
    1.13  
    1.14    @{text any} & = & @{text "prop  |  logic"} \\\\
    1.15  
    1.16    @{text prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\
    1.17      & @{text "|"} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
    1.18 -    & @{text "|"} & @{verbatim PROP} @{text aprop} \\
    1.19 +    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=?="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
    1.20      & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
    1.21 -    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=?="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
    1.22 +    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
    1.23      & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
    1.24 +    & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
    1.25      & @{text "|"} & @{verbatim "[|"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "|]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
    1.26 +    & @{text "|"} & @{text "\<lbrakk>"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{text "\<rbrakk>"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
    1.27      & @{text "|"} & @{verbatim "!!"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\
    1.28 -    & @{text "|"} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\\\
    1.29 +    & @{text "|"} & @{text "\<And>"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\
    1.30 +    & @{text "|"} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\
    1.31 +    & @{text "|"} & @{verbatim SORT_CONSTRAINT} @{verbatim "("} @{text type} @{verbatim ")"} \\
    1.32 +    & @{text "|"} & @{verbatim PROP} @{text aprop} \\\\
    1.33  
    1.34 -  @{text aprop} & = & @{text "id  |  longid  |  var  |  logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  "}@{verbatim "("} @{text any} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text any} @{verbatim ")"} \\\\
    1.35 +  @{text aprop} & = & @{text "id  |  longid  |  var  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "..."} \\
    1.36 +    & @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\\\
    1.37  
    1.38    @{text logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\
    1.39      & @{text "|"} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
    1.40 -    & @{text "|"} & @{text "id  |  longid  |  var  |  logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} @{verbatim "("} @{text any} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text any} @{verbatim ")"} \\
    1.41 +    & @{text "|"} & @{text "id  |  longid  |  var  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "..."} \\
    1.42 +    & @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\
    1.43      & @{text "|"} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
    1.44 +    & @{text "|"} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
    1.45 +    & @{text "|"} & @{verbatim CONST} @{text "id  |  "}@{verbatim CONST} @{text "longid"} \\
    1.46      & @{text "|"} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\
    1.47  
    1.48 -  @{text idts} & = & @{text "idt  |  idt\<^sup>(\<^sup>1\<^sup>) idts"} \\\\
    1.49 +  @{text idts} & = & @{text "idt  |  idt\<^sup>(\<^sup>1\<^sup>) idts"} & @{text "(0)"} \\\\
    1.50  
    1.51 -  @{text idt} & = & @{text "id  |  "}@{verbatim "("} @{text idt} @{verbatim ")"} \\
    1.52 -    & @{text "|"} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\
    1.53 +  @{text idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text "  |  id  |  "}@{verbatim "_"} \\
    1.54 +    & @{text "|"} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\
    1.55 +    & @{text "|"} & @{verbatim "_"} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\
    1.56  
    1.57 -  @{text pttrns} & = & @{text "pttrn  |  pttrn\<^sup>(\<^sup>1\<^sup>) pttrns"} \\\\
    1.58 +  @{text pttrns} & = & @{text "pttrn  |  pttrn\<^sup>(\<^sup>1\<^sup>) pttrns"} & @{text "(0)"} \\\\
    1.59  
    1.60    @{text pttrn} & = & @{text idt} \\\\
    1.61  
    1.62    @{text type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\
    1.63 -    & @{text "|"} & @{text "tid  |  tvar  |  tid"} @{verbatim "::"} @{text "sort  |  tvar  "}@{verbatim "::"} @{text sort} \\
    1.64 +    & @{text "|"} & @{text "tid  |  tvar  |  "}@{verbatim "_"} \\
    1.65 +    & @{text "|"} & @{text "tid"} @{verbatim "::"} @{text "sort  |  tvar  "}@{verbatim "::"} @{text "sort  |  "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\
    1.66      & @{text "|"} & @{text "id  |  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) id  |  "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text id} \\
    1.67      & @{text "|"} & @{text "longid  |  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) longid  |  "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text longid} \\
    1.68      & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
    1.69 -    & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\\\
    1.70 +    & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\
    1.71 +    & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
    1.72 +    & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\\\
    1.73  
    1.74 -  @{text sort} & = & @{text "id  |  longid  |  "}@{verbatim "{}"}@{text "  |  "}@{verbatim "{"} @{text "id | longid"}@{verbatim ","}@{text "\<dots>"}@{verbatim ","}@{text "id | longid"} @{verbatim "}"} \\
    1.75 -  \end{tabular}
    1.76 +  @{text sort} & = & @{text "id  |  longid  |  "}@{verbatim "{}"}@{text "  |  "}@{verbatim "{"} @{text "id | longid"} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text "id | longid"} @{verbatim "}"} \\
    1.77 +  \end{supertabular}
    1.78    \end{center}
    1.79 -  \caption{The Pure grammar}\label{fig:pure-grammar}
    1.80 -  \end{figure}
    1.81  
    1.82 -  The priority grammar of the @{text "Pure"} theory is defined in
    1.83 -  \figref{fig:pure-grammar}.  The following nonterminals are
    1.84 -  introduced:
    1.85 +  \medskip The following nonterminals are introduced here:
    1.86  
    1.87    \begin{description}
    1.88  
    1.89 @@ -571,24 +581,61 @@
    1.90  
    1.91    \end{description}
    1.92  
    1.93 -  \begin{warn}
    1.94 -  In @{text idts}, note that @{text "x :: nat y"} is parsed as @{text
    1.95 -  "x :: (nat y)"}, treating @{text y} like a type constructor applied
    1.96 -  to @{text nat}.  To avoid this interpretation, write @{text "(x ::
    1.97 -  nat) y"} with explicit parentheses.
    1.98 +  Some further explanations of certain syntax features are required.
    1.99  
   1.100 -  Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x ::
   1.101 +  \begin{itemize}
   1.102 +
   1.103 +  \item In @{text idts}, note that @{text "x :: nat y"} is parsed as
   1.104 +  @{text "x :: (nat y)"}, treating @{text y} like a type constructor
   1.105 +  applied to @{text nat}.  To avoid this interpretation, write @{text
   1.106 +  "(x :: nat) y"} with explicit parentheses.
   1.107 +
   1.108 +  \item Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x ::
   1.109    (nat y :: nat)"}.  The correct form is @{text "(x :: nat) (y ::
   1.110    nat)"}, or @{text "(x :: nat) y :: nat"} if @{text y} is last in the
   1.111    sequence of identifiers.
   1.112 -  \end{warn}
   1.113  
   1.114 -  \begin{warn}
   1.115 -  Type constraints for terms bind very weakly.  For example, @{text "x
   1.116 -  < y :: nat"} is normally parsed as @{text "(x < y) :: nat"}, unless
   1.117 -  @{text "<"} has a very low priority, in which case the input is
   1.118 -  likely to be ambiguous.  The correct form is @{text "x < (y :: nat)"}.
   1.119 -  \end{warn}
   1.120 +  \item Type constraints for terms bind very weakly.  For example,
   1.121 +  @{text "x < y :: nat"} is normally parsed as @{text "(x < y) ::
   1.122 +  nat"}, unless @{text "<"} has a very low priority, in which case the
   1.123 +  input is likely to be ambiguous.  The correct form is @{text "x < (y
   1.124 +  :: nat)"}.
   1.125 +
   1.126 +  \item Constraints may be either written with two literal colons
   1.127 +  ``@{verbatim "::"}'' or the double-colon symbol @{verbatim "\<Colon>"},
   1.128 +  which actually look exactly the same in some {\LaTeX} styles.
   1.129 +
   1.130 +  \item Placeholders @{verbatim "_"} may occur in different roles:
   1.131 +
   1.132 +  \begin{description}
   1.133 +
   1.134 +  \item A type @{text "_"} or @{text "_::sort"} acts like an anonymous
   1.135 +  type-inference parameter, which is filled-in according to the most
   1.136 +  general type produced by the type-checking phase.
   1.137 +
   1.138 +  \item A bound @{text "_"} refers to a vacuous abstraction, where the
   1.139 +  body does not refer to the binding introduced here.  As in @{term
   1.140 +  "\<lambda>x _. x"} (which is @{text "\<alpha>"}-equivalent to @{text "\<lambda>x y. x"}).
   1.141 +
   1.142 +  \item A free @{text "_"} refers to an implicit outer binding.
   1.143 +  Higher definitional packages usually allow forms like @{text "f x _
   1.144 +  = a"}.
   1.145 +
   1.146 +  \item A free @{text "_"} within a term pattern
   1.147 +  (\secref{sec:term-decls}) refers to an anonymous schematic variable
   1.148 +  that is implicitly abstracted over its context of locally bound
   1.149 +  variables.  This allows pattern matching of @{text "{x. x = a}
   1.150 +  (\<IS> {x. x = _})"}, for example.
   1.151 +
   1.152 +  \item The three literal dots ``@{verbatim "..."}'' may be also
   1.153 +  written as ellipsis symbol @{verbatim "\<dots>"}.  In both cases it refers
   1.154 +  to a special schematic variable, which is bound in the context.
   1.155 +  This special term abbreviation works nicely calculational resoning
   1.156 +  (\secref{sec:calculation}).
   1.157 +
   1.158 +  \end{description}
   1.159 +
   1.160 +  \end{itemize}
   1.161  *}
   1.162  
   1.163  

     2.1 --- a/doc-src/IsarRef/isar-ref.tex	Thu Nov 13 21:57:20 2008 +0100
     2.2 +++ b/doc-src/IsarRef/isar-ref.tex	Thu Nov 13 21:57:50 2008 +0100
     2.3 @@ -7,6 +7,7 @@
     2.4  \usepackage[nohyphen,strings]{../underscore}
     2.5  \usepackage{../isabelle,../isabellesym}
     2.6  \usepackage{../ttbox,,../rail,../railsetup}
     2.7 +\usepackage{supertabular}
     2.8  \usepackage{style}
     2.9  \usepackage{../pdfsetup}
    2.10