--- 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]:
--- 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
--- 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
--- 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%
--- 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
--- 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}%