author wenzelm Mon, 03 Oct 2011 11:14:19 +0200 changeset 45103 a45121ffcfcb parent 45102 7bb89635eb51 child 45104 0a3f301271ba
some amendments due to Jean Pichon;
--- 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}%
%
\end{isabellebody}%