# HG changeset patch
# User wenzelm
# Date 1317633259 -7200
# Node ID a45121ffcfcba08b5a9b0d8970b982152ac72366
# Parent  7bb89635eb51c7ff4baf9d3e43c13175236da229
some amendments due to Jean Pichon;

diff -r 7bb89635eb51 -r a45121ffcfcb doc-src/IsarRef/Thy/First_Order_Logic.thy
--- a/doc-src/IsarRef/Thy/First_Order_Logic.thy	Thu Sep 29 09:37:59 2011 +0200
+++ b/doc-src/IsarRef/Thy/First_Order_Logic.thy	Mon Oct 03 11:14:19 2011 +0200
@@ -47,7 +47,7 @@
 text {*
   \noindent Substitution is very powerful, but also hard to control in
   full generality.  We derive some common symmetry~/ transitivity
-  schemes of as particular consequences.
+  schemes of @{term equal} as particular consequences.
 *}
 
 theorem sym [sym]:
diff -r 7bb89635eb51 -r a45121ffcfcb doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Thu Sep 29 09:37:59 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Mon Oct 03 11:14:19 2011 +0200
@@ -129,7 +129,7 @@
   proof structure at all, but goes back right to the theory level.
   Furthermore, @{command "oops"} does not produce any result theorem
   --- there is no intended claim to be able to complete the proof
-  anyhow.
+  in any way.
 
   A typical application of @{command "oops"} is to explain Isar proofs
   \emph{within} the system itself, in conjunction with the document
diff -r 7bb89635eb51 -r a45121ffcfcb doc-src/IsarRef/Thy/Synopsis.thy
--- a/doc-src/IsarRef/Thy/Synopsis.thy	Thu Sep 29 09:37:59 2011 +0200
+++ b/doc-src/IsarRef/Thy/Synopsis.thy	Mon Oct 03 11:14:19 2011 +0200
@@ -907,7 +907,7 @@
 
 text {* There is nothing special about logical connectives (@{text
   "\<and>"}, @{text "\<or>"}, @{text "\<forall>"}, @{text "\<exists>"} etc.).  Operators from
-  set-theory or lattice-theory for analogously.  It is only a matter
+  set-theory or lattice-theory work analogously.  It is only a matter
   of rule declarations in the library; rules can be also specified
   explicitly.
 *}
@@ -1105,4 +1105,4 @@
   note `C`
 end
 
-end
\ No newline at end of file
+end
diff -r 7bb89635eb51 -r a45121ffcfcb doc-src/IsarRef/Thy/document/First_Order_Logic.tex
--- a/doc-src/IsarRef/Thy/document/First_Order_Logic.tex	Thu Sep 29 09:37:59 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/First_Order_Logic.tex	Mon Oct 03 11:14:19 2011 +0200
@@ -68,7 +68,7 @@
 \begin{isamarkuptext}%
 \noindent Substitution is very powerful, but also hard to control in
   full generality.  We derive some common symmetry~/ transitivity
-  schemes of as particular consequences.%
+  schemes of \isa{equal} as particular consequences.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{theorem}\isamarkupfalse%
diff -r 7bb89635eb51 -r a45121ffcfcb doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Thu Sep 29 09:37:59 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon Oct 03 11:14:19 2011 +0200
@@ -159,7 +159,7 @@
   proof structure at all, but goes back right to the theory level.
   Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem
   --- there is no intended claim to be able to complete the proof
-  anyhow.
+  in any way.
 
   A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
   \emph{within} the system itself, in conjunction with the document
diff -r 7bb89635eb51 -r a45121ffcfcb doc-src/IsarRef/Thy/document/Synopsis.tex
--- a/doc-src/IsarRef/Thy/document/Synopsis.tex	Thu Sep 29 09:37:59 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Synopsis.tex	Mon Oct 03 11:14:19 2011 +0200
@@ -2258,7 +2258,7 @@
 %
 \begin{isamarkuptext}%
 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
-  set-theory or lattice-theory for analogously.  It is only a matter
+  set-theory or lattice-theory work analogously.  It is only a matter
   of rule declarations in the library; rules can be also specified
   explicitly.%
 \end{isamarkuptext}%
@@ -2708,6 +2708,7 @@
 {\isafoldtheory}%
 %
 \isadelimtheory
+\isanewline
 %
 \endisadelimtheory
 \end{isabellebody}%