1.1 --- a/doc-src/IsarRef/Thy/First_Order_Logic.thy	Thu Sep 29 09:37:59 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/First_Order_Logic.thy	Mon Oct 03 11:14:19 2011 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4  text {*
     1.5    \noindent Substitution is very powerful, but also hard to control in
     1.6    full generality.  We derive some common symmetry~/ transitivity
     1.7 -  schemes of as particular consequences.
     1.8 +  schemes of @{term equal} as particular consequences.
     1.9  *}
    1.10  
    1.11  theorem sym [sym]:

     2.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Thu Sep 29 09:37:59 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Mon Oct 03 11:14:19 2011 +0200
     2.3 @@ -129,7 +129,7 @@
     2.4    proof structure at all, but goes back right to the theory level.
     2.5    Furthermore, @{command "oops"} does not produce any result theorem
     2.6    --- there is no intended claim to be able to complete the proof
     2.7 -  anyhow.
     2.8 +  in any way.
     2.9  
    2.10    A typical application of @{command "oops"} is to explain Isar proofs
    2.11    \emph{within} the system itself, in conjunction with the document

     3.1 --- a/doc-src/IsarRef/Thy/Synopsis.thy	Thu Sep 29 09:37:59 2011 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/Synopsis.thy	Mon Oct 03 11:14:19 2011 +0200
     3.3 @@ -907,7 +907,7 @@
     3.4  
     3.5  text {* There is nothing special about logical connectives (@{text
     3.6    "\<and>"}, @{text "\<or>"}, @{text "\<forall>"}, @{text "\<exists>"} etc.).  Operators from
     3.7 -  set-theory or lattice-theory for analogously.  It is only a matter
     3.8 +  set-theory or lattice-theory work analogously.  It is only a matter
     3.9    of rule declarations in the library; rules can be also specified
    3.10    explicitly.
    3.11  *}
    3.12 @@ -1105,4 +1105,4 @@
    3.13    note `C`
    3.14  end
    3.15  
    3.16 -end
    3.17 \ No newline at end of file
    3.18 +end

     4.1 --- a/doc-src/IsarRef/Thy/document/First_Order_Logic.tex	Thu Sep 29 09:37:59 2011 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/document/First_Order_Logic.tex	Mon Oct 03 11:14:19 2011 +0200
     4.3 @@ -68,7 +68,7 @@
     4.4  \begin{isamarkuptext}%
     4.5  \noindent Substitution is very powerful, but also hard to control in
     4.6    full generality.  We derive some common symmetry~/ transitivity
     4.7 -  schemes of as particular consequences.%
     4.8 +  schemes of \isa{equal} as particular consequences.%
     4.9  \end{isamarkuptext}%
    4.10  \isamarkuptrue%
    4.11  \isacommand{theorem}\isamarkupfalse%

     5.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Thu Sep 29 09:37:59 2011 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon Oct 03 11:14:19 2011 +0200
     5.3 @@ -159,7 +159,7 @@
     5.4    proof structure at all, but goes back right to the theory level.
     5.5    Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem
     5.6    --- there is no intended claim to be able to complete the proof
     5.7 -  anyhow.
     5.8 +  in any way.
     5.9  
    5.10    A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
    5.11    \emph{within} the system itself, in conjunction with the document

     6.1 --- a/doc-src/IsarRef/Thy/document/Synopsis.tex	Thu Sep 29 09:37:59 2011 +0200
     6.2 +++ b/doc-src/IsarRef/Thy/document/Synopsis.tex	Mon Oct 03 11:14:19 2011 +0200
     6.3 @@ -2258,7 +2258,7 @@
     6.4  %
     6.5  \begin{isamarkuptext}%
     6.6  There is nothing special about logical connectives (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616E643E}{\isasymand}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}{\isaliteral{22}{\isachardoublequote}}} etc.).  Operators from
     6.7 -  set-theory or lattice-theory for analogously.  It is only a matter
     6.8 +  set-theory or lattice-theory work analogously.  It is only a matter
     6.9    of rule declarations in the library; rules can be also specified
    6.10    explicitly.%
    6.11  \end{isamarkuptext}%
    6.12 @@ -2708,6 +2708,7 @@
    6.13  {\isafoldtheory}%
    6.14  %
    6.15  \isadelimtheory
    6.16 +\isanewline
    6.17  %
    6.18  \endisadelimtheory
    6.19  \end{isabellebody}%