# HG changeset patch
# User wenzelm
# Date 1136934662 -3600
# Node ID 8911c5a8b078dad8896178a5fc4eb08e1b0e181d
# Parent  b59766bc66c9a68bd400580bc99624e61c760875
updated;

diff -r b59766bc66c9 -r 8911c5a8b078 doc-src/AxClass/Group/document/isabellesym.sty
--- 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\,}}
diff -r b59766bc66c9 -r 8911c5a8b078 doc-src/IsarImplementation/Thy/document/integration.tex
--- 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.
diff -r b59766bc66c9 -r 8911c5a8b078 doc-src/IsarImplementation/Thy/document/isabellesym.sty
--- 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\,}}
diff -r b59766bc66c9 -r 8911c5a8b078 doc-src/IsarOverview/Isar/document/isabellesym.sty
--- 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\,}}
diff -r b59766bc66c9 -r 8911c5a8b078 doc-src/LaTeXsugar/Sugar/document/isabellesym.sty
--- 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\,}}
diff -r b59766bc66c9 -r 8911c5a8b078 doc-src/Locales/Locales/document/isabellesym.sty
--- 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\,}}
diff -r b59766bc66c9 -r 8911c5a8b078 doc-src/TutorialI/isabellesym.sty
--- 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\,}}
diff -r b59766bc66c9 -r 8911c5a8b078 doc-src/ZF/isabellesym.sty
--- 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\,}}