1.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:56:49 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:57:20 2008 +0100
     1.3 @@ -477,9 +477,43 @@
     1.4    \begin{center}
     1.5    \begin{tabular}{rclc}
     1.6  
     1.7 -    @{text any} & = & @{text "prop  |  logic"} \\\\
     1.8 -    % FIXME
     1.9 +  @{text any} & = & @{text "prop  |  logic"} \\\\
    1.10  
    1.11 +  @{text prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\
    1.12 +    & @{text "|"} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
    1.13 +    & @{text "|"} & @{verbatim PROP} @{text aprop} \\
    1.14 +    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
    1.15 +    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=?="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
    1.16 +    & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
    1.17 +    & @{text "|"} & @{verbatim "[|"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "|]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
    1.18 +    & @{text "|"} & @{verbatim "!!"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\
    1.19 +    & @{text "|"} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\\\
    1.20 +
    1.21 +  @{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.22 +
    1.23 +  @{text logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\
    1.24 +    & @{text "|"} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
    1.25 +    & @{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.26 +    & @{text "|"} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
    1.27 +    & @{text "|"} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\
    1.28 +
    1.29 +  @{text idts} & = & @{text "idt  |  idt\<^sup>(\<^sup>1\<^sup>) idts"} \\\\
    1.30 +
    1.31 +  @{text idt} & = & @{text "id  |  "}@{verbatim "("} @{text idt} @{verbatim ")"} \\
    1.32 +    & @{text "|"} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\
    1.33 +
    1.34 +  @{text pttrns} & = & @{text "pttrn  |  pttrn\<^sup>(\<^sup>1\<^sup>) pttrns"} \\\\
    1.35 +
    1.36 +  @{text pttrn} & = & @{text idt} \\\\
    1.37 +
    1.38 +  @{text type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\
    1.39 +    & @{text "|"} & @{text "tid  |  tvar  |  tid"} @{verbatim "::"} @{text "sort  |  tvar  "}@{verbatim "::"} @{text sort} \\
    1.40 +    & @{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.41 +    & @{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.42 +    & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
    1.43 +    & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\\\
    1.44 +
    1.45 +  @{text sort} & = & @{text "id  |  longid  |  "}@{verbatim "{}"}@{text "  |  "}@{verbatim "{"} @{text "id | longid"}@{verbatim ","}@{text "\<dots>"}@{verbatim ","}@{text "id | longid"} @{verbatim "}"} \\
    1.46    \end{tabular}
    1.47    \end{center}
    1.48    \caption{The Pure grammar}\label{fig:pure-grammar}