1.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Sun Feb 15 17:48:02 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Sun Feb 15 18:11:35 2009 +0100
     1.3 @@ -1,5 +1,3 @@
     1.4 -(* $Id$ *)
     1.5 -
     1.6  theory Proof
     1.7  imports Main
     1.8  begin
     1.9 @@ -10,8 +8,8 @@
    1.10    Proof commands perform transitions of Isar/VM machine
    1.11    configurations, which are block-structured, consisting of a stack of
    1.12    nodes with three main components: logical proof context, current
    1.13 -  facts, and open goals.  Isar/VM transitions are \emph{typed}
    1.14 -  according to the following three different modes of operation:
    1.15 +  facts, and open goals.  Isar/VM transitions are typed according to
    1.16 +  the following three different modes of operation:
    1.17  
    1.18    \begin{description}
    1.19  
    1.20 @@ -32,13 +30,17 @@
    1.21  
    1.22    \end{description}
    1.23  
    1.24 -  The proof mode indicator may be read as a verb telling the writer
    1.25 -  what kind of operation may be performed next.  The corresponding
    1.26 -  typings of proof commands restricts the shape of well-formed proof
    1.27 -  texts to particular command sequences.  So dynamic arrangements of
    1.28 -  commands eventually turn out as static texts of a certain structure.
    1.29 -  \Appref{ap:refcard} gives a simplified grammar of the overall
    1.30 -  (extensible) language emerging that way.
    1.31 +  The proof mode indicator may be understood as an instruction to the
    1.32 +  writer, telling what kind of operation may be performed next.  The
    1.33 +  corresponding typings of proof commands restricts the shape of
    1.34 +  well-formed proof texts to particular command sequences.  So dynamic
    1.35 +  arrangements of commands eventually turn out as static texts of a
    1.36 +  certain structure.
    1.37 +
    1.38 +  \Appref{ap:refcard} gives a simplified grammar of the (extensible)
    1.39 +  language emerging that way from the different types of proof
    1.40 +  commands.  The main ideas of the overall Isar framework are
    1.41 +  explained in \chref{ch:isar-framework}.
    1.42  *}
    1.43  
    1.44