1.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sun Feb 15 17:48:02 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sun Feb 15 18:11:35 2009 +0100
     1.3 @@ -1,5 +1,3 @@
     1.4 -(* $Id$ *)
     1.5 -
     1.6  theory Inner_Syntax
     1.7  imports Main
     1.8  begin
     1.9 @@ -370,7 +368,7 @@
    1.10    \end{matharray}
    1.11  
    1.12    \begin{rail}
    1.13 -    ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
    1.14 +    ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
    1.15      ;
    1.16    \end{rail}
    1.17  
    1.18 @@ -525,13 +523,15 @@
    1.19      & @{text "|"} & @{text "tid  |  tvar  |  "}@{verbatim "_"} \\
    1.20      & @{text "|"} & @{text "tid"} @{verbatim "::"} @{text "sort  |  tvar  "}@{verbatim "::"} @{text "sort  |  "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\
    1.21      & @{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.22 -    & @{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.23 +    & @{text "|"} & @{text "longid  |  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) longid"} \\
    1.24 +    & @{text "|"} & @{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text longid} \\
    1.25      & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
    1.26      & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\
    1.27      & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
    1.28      & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\\\
    1.29  
    1.30 -  @{syntax_def (inner) sort} & = & @{text "id  |  longid  |  "}@{verbatim "{}"}@{text "  |  "}@{verbatim "{"} @{text "(id | longid)"} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text "(id | longid)"} @{verbatim "}"} \\
    1.31 +  @{syntax_def (inner) sort} & = & @{text "id  |  longid  |  "}@{verbatim "{}"} \\
    1.32 +    & @{text "|"} & @{verbatim "{"} @{text "(id | longid)"} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text "(id | longid)"} @{verbatim "}"} \\
    1.33    \end{supertabular}
    1.34    \end{center}
    1.35  

     2.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Sun Feb 15 17:48:02 2009 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Sun Feb 15 18:11:35 2009 +0100
     2.3 @@ -1,5 +1,3 @@
     2.4 -(* $Id$ *)
     2.5 -
     2.6  theory Proof
     2.7  imports Main
     2.8  begin
     2.9 @@ -10,8 +8,8 @@
    2.10    Proof commands perform transitions of Isar/VM machine
    2.11    configurations, which are block-structured, consisting of a stack of
    2.12    nodes with three main components: logical proof context, current
    2.13 -  facts, and open goals.  Isar/VM transitions are \emph{typed}
    2.14 -  according to the following three different modes of operation:
    2.15 +  facts, and open goals.  Isar/VM transitions are typed according to
    2.16 +  the following three different modes of operation:
    2.17  
    2.18    \begin{description}
    2.19  
    2.20 @@ -32,13 +30,17 @@
    2.21  
    2.22    \end{description}
    2.23  
    2.24 -  The proof mode indicator may be read as a verb telling the writer
    2.25 -  what kind of operation may be performed next.  The corresponding
    2.26 -  typings of proof commands restricts the shape of well-formed proof
    2.27 -  texts to particular command sequences.  So dynamic arrangements of
    2.28 -  commands eventually turn out as static texts of a certain structure.
    2.29 -  \Appref{ap:refcard} gives a simplified grammar of the overall
    2.30 -  (extensible) language emerging that way.
    2.31 +  The proof mode indicator may be understood as an instruction to the
    2.32 +  writer, telling what kind of operation may be performed next.  The
    2.33 +  corresponding typings of proof commands restricts the shape of
    2.34 +  well-formed proof texts to particular command sequences.  So dynamic
    2.35 +  arrangements of commands eventually turn out as static texts of a
    2.36 +  certain structure.
    2.37 +
    2.38 +  \Appref{ap:refcard} gives a simplified grammar of the (extensible)
    2.39 +  language emerging that way from the different types of proof
    2.40 +  commands.  The main ideas of the overall Isar framework are
    2.41 +  explained in \chref{ch:isar-framework}.
    2.42  *}
    2.43  
    2.44