summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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}% % \isadelimtheory +\isanewline % \endisadelimtheory \end{isabellebody}%