--- a/doc-src/AxClass/Group/document/isabellesym.sty Tue Jan 10 19:36:59 2006 +0100
+++ b/doc-src/AxClass/Group/document/isabellesym.sty Wed Jan 11 00:11:02 2006 +0100
@@ -181,12 +181,13 @@
\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
-\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
\newcommand{\isasymup}{\isamath{\uparrow}}
\newcommand{\isasymUp}{\isamath{\Uparrow}}
\newcommand{\isasymdown}{\isamath{\downarrow}}
@@ -207,8 +208,6 @@
\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
-\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
-\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbottom}{\isamath{\bot}}
\newcommand{\isasymtop}{\isamath{\top}}
\newcommand{\isasymand}{\isamath{\wedge}}
@@ -218,6 +217,7 @@
\newcommand{\isasymforall}{\isamath{\forall\,}}
\newcommand{\isasymexists}{\isamath{\exists\,}}
\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
+\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
\newcommand{\isasymturnstile}{\isamath{\vdash}}
@@ -252,6 +252,8 @@
\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
\newcommand{\isasymsqinter}{\isamath{\sqcap}}
\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
+\newcommand{\isasymsetminus}{\isamath{\setminus}}
+\newcommand{\isasympropto}{\isamath{\propto}}
\newcommand{\isasymuplus}{\isamath{\uplus}}
\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
\newcommand{\isasymnoteq}{\isamath{\not=}}
@@ -264,8 +266,6 @@
\newcommand{\isasymsmile}{\isamath{\smile}}
\newcommand{\isasymequiv}{\isamath{\equiv}}
\newcommand{\isasymfrown}{\isamath{\frown}}
-\newcommand{\isasympropto}{\isamath{\propto}}
-\newcommand{\isasymsome}{\isamath{\epsilon\,}}
\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
\newcommand{\isasymbowtie}{\isamath{\bowtie}}
\newcommand{\isasymprec}{\isamath{\prec}}
@@ -357,3 +357,4 @@
\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
\newcommand{\isasymspacespace}{\isamath{~~}}
\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
--- a/doc-src/IsarImplementation/Thy/document/integration.tex Tue Jan 10 19:36:59 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Wed Jan 11 00:11:02 2006 +0100
@@ -181,8 +181,6 @@
\verb| Toplevel.transition -> Toplevel.transition| \\
\indexml{Toplevel.theory-to-proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
\verb| Toplevel.transition -> Toplevel.transition| \\
- \indexml{Toplevel.theory-theory-to-proof}\verb|Toplevel.theory_theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
-\verb| Toplevel.transition -> Toplevel.transition| \\
\indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
\verb| Toplevel.transition -> Toplevel.transition| \\
\indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
@@ -205,13 +203,10 @@
\item \verb|Toplevel.theory| adjoins a theory transformer.
\item \verb|Toplevel.theory_to_proof| adjoins a global goal function,
- which turns a theory into a proof state. The theory must not be
- changed here! The generic Isar goal setup includes an argument that
- specifies how to apply the proven result to the theory, when the
- proof is finished.
-
- \item \verb|Toplevel.theory_theory_to_proof| is like \verb|Toplevel.theory_to_proof|, but allows the initial theory to be
- changed before entering proof state.
+ which turns a theory into a proof state. The theory may be changed
+ before entering the proof; the generic Isar goal setup includes an
+ argument that specifies how to apply the proven result to the
+ theory, when the proof is finished.
\item \verb|Toplevel.proof| adjoins a deterministic proof command,
with a singleton result state.
--- a/doc-src/IsarImplementation/Thy/document/isabellesym.sty Tue Jan 10 19:36:59 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/isabellesym.sty Wed Jan 11 00:11:02 2006 +0100
@@ -181,12 +181,13 @@
\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
-\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
\newcommand{\isasymup}{\isamath{\uparrow}}
\newcommand{\isasymUp}{\isamath{\Uparrow}}
\newcommand{\isasymdown}{\isamath{\downarrow}}
@@ -207,8 +208,6 @@
\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
-\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
-\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbottom}{\isamath{\bot}}
\newcommand{\isasymtop}{\isamath{\top}}
\newcommand{\isasymand}{\isamath{\wedge}}
@@ -218,6 +217,7 @@
\newcommand{\isasymforall}{\isamath{\forall\,}}
\newcommand{\isasymexists}{\isamath{\exists\,}}
\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
+\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
\newcommand{\isasymturnstile}{\isamath{\vdash}}
@@ -252,6 +252,8 @@
\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
\newcommand{\isasymsqinter}{\isamath{\sqcap}}
\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
+\newcommand{\isasymsetminus}{\isamath{\setminus}}
+\newcommand{\isasympropto}{\isamath{\propto}}
\newcommand{\isasymuplus}{\isamath{\uplus}}
\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
\newcommand{\isasymnoteq}{\isamath{\not=}}
@@ -264,8 +266,6 @@
\newcommand{\isasymsmile}{\isamath{\smile}}
\newcommand{\isasymequiv}{\isamath{\equiv}}
\newcommand{\isasymfrown}{\isamath{\frown}}
-\newcommand{\isasympropto}{\isamath{\propto}}
-\newcommand{\isasymsome}{\isamath{\epsilon\,}}
\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
\newcommand{\isasymbowtie}{\isamath{\bowtie}}
\newcommand{\isasymprec}{\isamath{\prec}}
@@ -357,3 +357,4 @@
\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
\newcommand{\isasymspacespace}{\isamath{~~}}
\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
--- a/doc-src/IsarOverview/Isar/document/isabellesym.sty Tue Jan 10 19:36:59 2006 +0100
+++ b/doc-src/IsarOverview/Isar/document/isabellesym.sty Wed Jan 11 00:11:02 2006 +0100
@@ -181,12 +181,13 @@
\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
-\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
\newcommand{\isasymup}{\isamath{\uparrow}}
\newcommand{\isasymUp}{\isamath{\Uparrow}}
\newcommand{\isasymdown}{\isamath{\downarrow}}
@@ -207,8 +208,6 @@
\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
-\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
-\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbottom}{\isamath{\bot}}
\newcommand{\isasymtop}{\isamath{\top}}
\newcommand{\isasymand}{\isamath{\wedge}}
@@ -218,6 +217,7 @@
\newcommand{\isasymforall}{\isamath{\forall\,}}
\newcommand{\isasymexists}{\isamath{\exists\,}}
\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
+\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
\newcommand{\isasymturnstile}{\isamath{\vdash}}
@@ -252,6 +252,8 @@
\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
\newcommand{\isasymsqinter}{\isamath{\sqcap}}
\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
+\newcommand{\isasymsetminus}{\isamath{\setminus}}
+\newcommand{\isasympropto}{\isamath{\propto}}
\newcommand{\isasymuplus}{\isamath{\uplus}}
\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
\newcommand{\isasymnoteq}{\isamath{\not=}}
@@ -264,8 +266,6 @@
\newcommand{\isasymsmile}{\isamath{\smile}}
\newcommand{\isasymequiv}{\isamath{\equiv}}
\newcommand{\isasymfrown}{\isamath{\frown}}
-\newcommand{\isasympropto}{\isamath{\propto}}
-\newcommand{\isasymsome}{\isamath{\epsilon\,}}
\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
\newcommand{\isasymbowtie}{\isamath{\bowtie}}
\newcommand{\isasymprec}{\isamath{\prec}}
@@ -357,3 +357,4 @@
\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
\newcommand{\isasymspacespace}{\isamath{~~}}
\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
--- a/doc-src/LaTeXsugar/Sugar/document/isabellesym.sty Tue Jan 10 19:36:59 2006 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/isabellesym.sty Wed Jan 11 00:11:02 2006 +0100
@@ -181,12 +181,13 @@
\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
-\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
\newcommand{\isasymup}{\isamath{\uparrow}}
\newcommand{\isasymUp}{\isamath{\Uparrow}}
\newcommand{\isasymdown}{\isamath{\downarrow}}
@@ -207,8 +208,6 @@
\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
-\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
-\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbottom}{\isamath{\bot}}
\newcommand{\isasymtop}{\isamath{\top}}
\newcommand{\isasymand}{\isamath{\wedge}}
@@ -218,6 +217,7 @@
\newcommand{\isasymforall}{\isamath{\forall\,}}
\newcommand{\isasymexists}{\isamath{\exists\,}}
\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
+\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
\newcommand{\isasymturnstile}{\isamath{\vdash}}
@@ -252,6 +252,8 @@
\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
\newcommand{\isasymsqinter}{\isamath{\sqcap}}
\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
+\newcommand{\isasymsetminus}{\isamath{\setminus}}
+\newcommand{\isasympropto}{\isamath{\propto}}
\newcommand{\isasymuplus}{\isamath{\uplus}}
\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
\newcommand{\isasymnoteq}{\isamath{\not=}}
@@ -264,8 +266,6 @@
\newcommand{\isasymsmile}{\isamath{\smile}}
\newcommand{\isasymequiv}{\isamath{\equiv}}
\newcommand{\isasymfrown}{\isamath{\frown}}
-\newcommand{\isasympropto}{\isamath{\propto}}
-\newcommand{\isasymsome}{\isamath{\epsilon\,}}
\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
\newcommand{\isasymbowtie}{\isamath{\bowtie}}
\newcommand{\isasymprec}{\isamath{\prec}}
@@ -357,3 +357,4 @@
\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
\newcommand{\isasymspacespace}{\isamath{~~}}
\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
--- a/doc-src/Locales/Locales/document/isabellesym.sty Tue Jan 10 19:36:59 2006 +0100
+++ b/doc-src/Locales/Locales/document/isabellesym.sty Wed Jan 11 00:11:02 2006 +0100
@@ -181,12 +181,13 @@
\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
-\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
\newcommand{\isasymup}{\isamath{\uparrow}}
\newcommand{\isasymUp}{\isamath{\Uparrow}}
\newcommand{\isasymdown}{\isamath{\downarrow}}
@@ -207,8 +208,6 @@
\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
-\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
-\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbottom}{\isamath{\bot}}
\newcommand{\isasymtop}{\isamath{\top}}
\newcommand{\isasymand}{\isamath{\wedge}}
@@ -218,6 +217,7 @@
\newcommand{\isasymforall}{\isamath{\forall\,}}
\newcommand{\isasymexists}{\isamath{\exists\,}}
\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
+\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
\newcommand{\isasymturnstile}{\isamath{\vdash}}
@@ -252,6 +252,8 @@
\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
\newcommand{\isasymsqinter}{\isamath{\sqcap}}
\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
+\newcommand{\isasymsetminus}{\isamath{\setminus}}
+\newcommand{\isasympropto}{\isamath{\propto}}
\newcommand{\isasymuplus}{\isamath{\uplus}}
\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
\newcommand{\isasymnoteq}{\isamath{\not=}}
@@ -264,8 +266,6 @@
\newcommand{\isasymsmile}{\isamath{\smile}}
\newcommand{\isasymequiv}{\isamath{\equiv}}
\newcommand{\isasymfrown}{\isamath{\frown}}
-\newcommand{\isasympropto}{\isamath{\propto}}
-\newcommand{\isasymsome}{\isamath{\epsilon\,}}
\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
\newcommand{\isasymbowtie}{\isamath{\bowtie}}
\newcommand{\isasymprec}{\isamath{\prec}}
@@ -357,3 +357,4 @@
\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
\newcommand{\isasymspacespace}{\isamath{~~}}
\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
--- a/doc-src/TutorialI/isabellesym.sty Tue Jan 10 19:36:59 2006 +0100
+++ b/doc-src/TutorialI/isabellesym.sty Wed Jan 11 00:11:02 2006 +0100
@@ -181,12 +181,13 @@
\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
-\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
\newcommand{\isasymup}{\isamath{\uparrow}}
\newcommand{\isasymUp}{\isamath{\Uparrow}}
\newcommand{\isasymdown}{\isamath{\downarrow}}
@@ -207,8 +208,6 @@
\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
-\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
-\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbottom}{\isamath{\bot}}
\newcommand{\isasymtop}{\isamath{\top}}
\newcommand{\isasymand}{\isamath{\wedge}}
@@ -218,6 +217,7 @@
\newcommand{\isasymforall}{\isamath{\forall\,}}
\newcommand{\isasymexists}{\isamath{\exists\,}}
\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
+\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
\newcommand{\isasymturnstile}{\isamath{\vdash}}
@@ -252,6 +252,8 @@
\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
\newcommand{\isasymsqinter}{\isamath{\sqcap}}
\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
+\newcommand{\isasymsetminus}{\isamath{\setminus}}
+\newcommand{\isasympropto}{\isamath{\propto}}
\newcommand{\isasymuplus}{\isamath{\uplus}}
\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
\newcommand{\isasymnoteq}{\isamath{\not=}}
@@ -264,8 +266,6 @@
\newcommand{\isasymsmile}{\isamath{\smile}}
\newcommand{\isasymequiv}{\isamath{\equiv}}
\newcommand{\isasymfrown}{\isamath{\frown}}
-\newcommand{\isasympropto}{\isamath{\propto}}
-\newcommand{\isasymsome}{\isamath{\epsilon\,}}
\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
\newcommand{\isasymbowtie}{\isamath{\bowtie}}
\newcommand{\isasymprec}{\isamath{\prec}}
@@ -357,3 +357,4 @@
\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
\newcommand{\isasymspacespace}{\isamath{~~}}
\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
--- a/doc-src/ZF/isabellesym.sty Tue Jan 10 19:36:59 2006 +0100
+++ b/doc-src/ZF/isabellesym.sty Wed Jan 11 00:11:02 2006 +0100
@@ -181,12 +181,13 @@
\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
-\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
\newcommand{\isasymup}{\isamath{\uparrow}}
\newcommand{\isasymUp}{\isamath{\Uparrow}}
\newcommand{\isasymdown}{\isamath{\downarrow}}
@@ -207,8 +208,6 @@
\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
-\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
-\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbottom}{\isamath{\bot}}
\newcommand{\isasymtop}{\isamath{\top}}
\newcommand{\isasymand}{\isamath{\wedge}}
@@ -218,6 +217,7 @@
\newcommand{\isasymforall}{\isamath{\forall\,}}
\newcommand{\isasymexists}{\isamath{\exists\,}}
\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
+\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
\newcommand{\isasymturnstile}{\isamath{\vdash}}
@@ -252,6 +252,8 @@
\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
\newcommand{\isasymsqinter}{\isamath{\sqcap}}
\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
+\newcommand{\isasymsetminus}{\isamath{\setminus}}
+\newcommand{\isasympropto}{\isamath{\propto}}
\newcommand{\isasymuplus}{\isamath{\uplus}}
\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
\newcommand{\isasymnoteq}{\isamath{\not=}}
@@ -264,8 +266,6 @@
\newcommand{\isasymsmile}{\isamath{\smile}}
\newcommand{\isasymequiv}{\isamath{\equiv}}
\newcommand{\isasymfrown}{\isamath{\frown}}
-\newcommand{\isasympropto}{\isamath{\propto}}
-\newcommand{\isasymsome}{\isamath{\epsilon\,}}
\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
\newcommand{\isasymbowtie}{\isamath{\bowtie}}
\newcommand{\isasymprec}{\isamath{\prec}}
@@ -357,3 +357,4 @@
\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
\newcommand{\isasymspacespace}{\isamath{~~}}
\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}