# HG changeset patch
# User wenzelm
# Date 1254421256 -7200
# Node ID 3a2fa964ad08d34311ff9b8c5ffa15a3f032da45
# Parent  4602cb6ae0b558d84071f58affb0746aee65be32# Parent  4c6e3e7ac2bf1a9a4109fe4cf757fe73a3fc6dd1
merged

diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/Codegen/Thy/Setup.thy
--- a/doc-src/Codegen/Thy/Setup.thy	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy	Thu Oct 01 20:20:56 2009 +0200
@@ -10,6 +10,6 @@
    "~~/src/HOL/Decision_Procs/Ferrack"] *}
 
 ML_command {* Code_Target.code_width := 74 *}
-ML_command {* reset unique_names *}
+ML_command {* Unsynchronized.reset unique_names *}
 
 end
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarImplementation/Thy/Integration.thy
--- a/doc-src/IsarImplementation/Thy/Integration.thy	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/Integration.thy	Thu Oct 01 20:20:56 2009 +0200
@@ -59,9 +59,9 @@
   @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
   @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
   @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
-  @{index_ML Toplevel.debug: "bool ref"} \\
-  @{index_ML Toplevel.timing: "bool ref"} \\
-  @{index_ML Toplevel.profiling: "int ref"} \\
+  @{index_ML Toplevel.debug: "bool Unsynchronized.ref"} \\
+  @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
+  @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
   \end{mldecls}
 
   \begin{description}
@@ -85,11 +85,11 @@
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
   state if available, otherwise raises @{ML Toplevel.UNDEF}.
 
-  \item @{ML "set Toplevel.debug"} makes the toplevel print further
+  \item @{ML "Toplevel.debug := true"} makes the toplevel print further
   details about internal error conditions, exceptions being raised
   etc.
 
-  \item @{ML "set Toplevel.timing"} makes the toplevel print timing
+  \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
   information for each Isar command being executed.
 
   \item @{ML Toplevel.profiling}~@{verbatim ":="}~@{text "n"} controls
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Thu Oct 01 20:20:56 2009 +0200
@@ -547,7 +547,7 @@
   \end{mldecls}
   \begin{mldecls}
   @{index_ML_type thm} \\
-  @{index_ML proofs: "int ref"} \\
+  @{index_ML proofs: "int Unsynchronized.ref"} \\
   @{index_ML Thm.assume: "cterm -> thm"} \\
   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Thu Oct 01 20:20:56 2009 +0200
@@ -258,7 +258,7 @@
   \begin{mldecls}
   @{index_ML NAMED_CRITICAL: "string -> (unit -> 'a) -> 'a"} \\
   @{index_ML CRITICAL: "(unit -> 'a) -> 'a"} \\
-  @{index_ML setmp: "'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c"} \\
+  @{index_ML setmp: "'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c"} \\
   \end{mldecls}
 
   \begin{description}
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarImplementation/Thy/document/Integration.tex
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex	Thu Oct 01 20:20:56 2009 +0200
@@ -86,9 +86,9 @@
   \indexdef{}{ML}{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
   \indexdef{}{ML}{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
   \indexdef{}{ML}{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
-  \indexdef{}{ML}{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
-  \indexdef{}{ML}{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
-  \indexdef{}{ML}{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
+  \indexdef{}{ML}{Toplevel.debug}\verb|Toplevel.debug: bool Unsynchronized.ref| \\
+  \indexdef{}{ML}{Toplevel.timing}\verb|Toplevel.timing: bool Unsynchronized.ref| \\
+  \indexdef{}{ML}{Toplevel.profiling}\verb|Toplevel.profiling: int Unsynchronized.ref| \\
   \end{mldecls}
 
   \begin{description}
@@ -112,11 +112,11 @@
   \item \verb|Toplevel.proof_of|~\isa{state} selects the Isar proof
   state if available, otherwise raises \verb|Toplevel.UNDEF|.
 
-  \item \verb|set Toplevel.debug| makes the toplevel print further
+  \item \verb|Toplevel.debug := true| makes the toplevel print further
   details about internal error conditions, exceptions being raised
   etc.
 
-  \item \verb|set Toplevel.timing| makes the toplevel print timing
+  \item \verb|Toplevel.timing := true| makes the toplevel print timing
   information for each Isar command being executed.
 
   \item \verb|Toplevel.profiling|~\verb|:=|~\isa{n} controls
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarImplementation/Thy/document/Logic.tex
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Thu Oct 01 20:20:56 2009 +0200
@@ -546,7 +546,7 @@
   \end{mldecls}
   \begin{mldecls}
   \indexdef{}{ML type}{thm}\verb|type thm| \\
-  \indexdef{}{ML}{proofs}\verb|proofs: int ref| \\
+  \indexdef{}{ML}{proofs}\verb|proofs: int Unsynchronized.ref| \\
   \indexdef{}{ML}{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
   \indexdef{}{ML}{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
   \indexdef{}{ML}{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Oct 01 20:20:56 2009 +0200
@@ -277,7 +277,7 @@
 \begin{mldecls}
   \indexdef{}{ML}{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
   \indexdef{}{ML}{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
-  \indexdef{}{ML}{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
+  \indexdef{}{ML}{setmp}\verb|setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
   \end{mldecls}
 
   \begin{description}
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarOverview/Isar/Logic.thy
--- a/doc-src/IsarOverview/Isar/Logic.thy	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarOverview/Isar/Logic.thy	Thu Oct 01 20:20:56 2009 +0200
@@ -526,7 +526,6 @@
 tendency to use the default introduction and elimination rules to
 decompose goals and facts. This can lead to very tedious proofs:
 *}
-(*<*)ML"set quick_and_dirty"(*>*)
 lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y"
 proof
   fix x show "\<forall>y. A x y \<and> B x y \<longrightarrow> C x y"
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarOverview/Isar/ROOT.ML
--- a/doc-src/IsarOverview/Isar/ROOT.ML	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarOverview/Isar/ROOT.ML	Thu Oct 01 20:20:56 2009 +0200
@@ -1,2 +1,3 @@
-use_thy "Logic";
-use_thy "Induction"
+Unsynchronized.set quick_and_dirty;
+
+use_thys ["Logic", "Induction"];
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarOverview/Isar/document/Logic.tex
--- a/doc-src/IsarOverview/Isar/document/Logic.tex	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex	Thu Oct 01 20:20:56 2009 +0200
@@ -1228,19 +1228,6 @@
 decompose goals and facts. This can lead to very tedious proofs:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
 \isacommand{lemma}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
 %
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Oct 01 20:20:56 2009 +0200
@@ -96,19 +96,19 @@
 
 text {*
   \begin{mldecls} 
-    @{index_ML show_types: "bool ref"} & default @{ML false} \\
-    @{index_ML show_sorts: "bool ref"} & default @{ML false} \\
-    @{index_ML show_consts: "bool ref"} & default @{ML false} \\
-    @{index_ML long_names: "bool ref"} & default @{ML false} \\
-    @{index_ML short_names: "bool ref"} & default @{ML false} \\
-    @{index_ML unique_names: "bool ref"} & default @{ML true} \\
-    @{index_ML show_brackets: "bool ref"} & default @{ML false} \\
-    @{index_ML eta_contract: "bool ref"} & default @{ML true} \\
-    @{index_ML goals_limit: "int ref"} & default @{ML 10} \\
-    @{index_ML Proof.show_main_goal: "bool ref"} & default @{ML false} \\
-    @{index_ML show_hyps: "bool ref"} & default @{ML false} \\
-    @{index_ML show_tags: "bool ref"} & default @{ML false} \\
-    @{index_ML show_question_marks: "bool ref"} & default @{ML true} \\
+    @{index_ML show_types: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_sorts: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_consts: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\
+    @{index_ML show_brackets: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML eta_contract: "bool Unsynchronized.ref"} & default @{ML true} \\
+    @{index_ML goals_limit: "int Unsynchronized.ref"} & default @{ML 10} \\
+    @{index_ML Proof.show_main_goal: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_hyps: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_tags: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_question_marks: "bool Unsynchronized.ref"} & default @{ML true} \\
   \end{mldecls}
 
   These global ML variables control the detail of information that is
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarRef/Thy/ROOT-HOLCF.ML
--- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Thu Oct 01 20:20:56 2009 +0200
@@ -1,4 +1,4 @@
-set ThyOutput.source;
+Unsynchronized.set ThyOutput.source;
 use "../../antiquote_setup.ML";
 
 use_thy "HOLCF_Specific";
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarRef/Thy/ROOT-ZF.ML
--- a/doc-src/IsarRef/Thy/ROOT-ZF.ML	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML	Thu Oct 01 20:20:56 2009 +0200
@@ -1,4 +1,4 @@
-set ThyOutput.source;
+Unsynchronized.set ThyOutput.source;
 use "../../antiquote_setup.ML";
 
 use_thy "ZF_Specific";
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarRef/Thy/ROOT.ML
--- a/doc-src/IsarRef/Thy/ROOT.ML	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML	Thu Oct 01 20:20:56 2009 +0200
@@ -1,5 +1,5 @@
-set quick_and_dirty;
-set ThyOutput.source;
+Unsynchronized.set quick_and_dirty;
+Unsynchronized.set ThyOutput.source;
 use "../../antiquote_setup.ML";
 
 use_thys [
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Oct 01 20:20:56 2009 +0200
@@ -118,19 +118,19 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls} 
-    \indexdef{}{ML}{show\_types}\verb|show_types: bool ref| & default \verb|false| \\
-    \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\
-    \indexdef{}{ML}{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\
-    \indexdef{}{ML}{long\_names}\verb|long_names: bool ref| & default \verb|false| \\
-    \indexdef{}{ML}{short\_names}\verb|short_names: bool ref| & default \verb|false| \\
-    \indexdef{}{ML}{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\
-    \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\
-    \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\
-    \indexdef{}{ML}{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\
-    \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\
-    \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\
-    \indexdef{}{ML}{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\
-    \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\
+    \indexdef{}{ML}{show\_types}\verb|show_types: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
+    \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Unsynchronized.ref| & default \verb|true| \\
+    \indexdef{}{ML}{goals\_limit}\verb|goals_limit: int Unsynchronized.ref| & default \verb|10| \\
+    \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Unsynchronized.ref| & default \verb|true| \\
   \end{mldecls}
 
   These global ML variables control the detail of information that is
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/LaTeXsugar/IsaMakefile
--- a/doc-src/LaTeXsugar/IsaMakefile	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/LaTeXsugar/IsaMakefile	Thu Oct 01 20:20:56 2009 +0200
@@ -14,7 +14,7 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -g false -d false -D document
+USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -g false -d false -D document -M 1
 
 
 ## Sugar
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Oct 01 20:20:56 2009 +0200
@@ -143,7 +143,7 @@
 internal index. This can be avoided by turning the last digit into a
 subscript: write \verb!x\<^isub>1! and obtain the much nicer @{text"x\<^isub>1"}. *}
 
-(*<*)ML"reset show_question_marks"(*>*)
+(*<*)ML"Unsynchronized.reset show_question_marks"(*>*)
 
 subsection {*Qualified names*}
 
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/Locales/Locales/document/Examples3.tex
--- a/doc-src/Locales/Locales/document/Examples3.tex	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Thu Oct 01 20:20:56 2009 +0200
@@ -42,7 +42,7 @@
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
 \ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ nat{\isacharunderscore}less{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
@@ -101,13 +101,12 @@
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
 \ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
-\ lattice{\isacharcolon}\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}%
+\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptxt}%
 We have already shown that this is a partial order,%
 \end{isamarkuptxt}%
@@ -134,21 +133,12 @@
 \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ arith{\isacharplus}%
 \begin{isamarkuptxt}%
-For the first of the equations, we refer to the theorem
-  shown in the previous interpretation.%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ nat{\isacharunderscore}less{\isacharunderscore}eq{\isacharparenright}%
-\begin{isamarkuptxt}%
-In order to show the remaining equations, we put ourselves in a
+In order to show the equations, we put ourselves in a
     situation where the lattice theorems can be used in a convenient way.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\ \ \isacommand{from}\isamarkupfalse%
-\ lattice\ \isacommand{interpret}\isamarkupfalse%
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{interpret}\isamarkupfalse%
 \ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{show}\isamarkupfalse%
@@ -180,45 +170,8 @@
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
 \ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}total{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales\ arith\isanewline
-\isacommand{qed}\isamarkupfalse%
-\ {\isacharparenleft}rule\ nat{\isacharunderscore}less{\isacharunderscore}eq\ nat{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}join{\isacharunderscore}eq{\isacharparenright}{\isacharplus}%
-\endisatagvisible
-{\isafoldvisible}%
-%
-\isadelimvisible
-%
-\endisadelimvisible
-%
-\begin{isamarkuptext}%
-Since the locale hierarchy reflects that total
-  orders are distributive lattices, an explicit interpretation of
-  distributive lattices for the order relation on natural numbers is
-  only necessary for mapping the definitions to the right operators on
-  \isa{nat}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimvisible
-%
-\endisadelimvisible
-%
-\isatagvisible
-\isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales\ {\isacharbrackleft}{\isadigit{1}}{\isacharbrackright}\ {\isacharparenleft}rule\ nat{\isacharunderscore}less{\isacharunderscore}eq\ nat{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}join{\isacharunderscore}eq{\isacharparenright}{\isacharplus}%
+\ unfold{\isacharunderscore}locales\ arith%
 \endisatagvisible
 {\isafoldvisible}%
 %
@@ -248,7 +201,30 @@
 \hrule
 \caption{Interpreted theorems for \isa{{\isasymle}} on the natural numbers.}
 \label{tab:nat-lattice}
-\end{table}%
+\end{table}
+
+  Note that since the locale hierarchy reflects that total orders are
+  distributive lattices, an explicit interpretation of distributive
+  lattices for the order relation on natural numbers is not neccessary.
+
+  Why not push this idea further and just give the last interpretation
+  as a single interpretation instead of the sequence of three?  The
+  reasons for this are twofold:
+\begin{itemize}
+\item
+  Often it is easier to work in an incremental fashion, because later
+  interpretations require theorems provided by earlier
+  interpretations.
+\item
+  Assume that a definition is made in some locale $l_1$, and that $l_2$
+  imports $l_1$.  Let an equation for the definition be
+  proved in an interpretation of $l_2$.  The equation will be unfolded
+  in interpretations of theorems added to $l_2$ or below in the import
+  hierarchy, but not for theorems added above $l_2$.
+  Hence, an equation interpreting a definition should always be given in
+  an interpretation of the locale where the definition is made, not in
+  an interpretation of a locale further down the hierarchy.
+\end{itemize}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -264,8 +240,7 @@
 \isamarkuptrue%
 \isacommand{interpretation}\isamarkupfalse%
 \ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharcolon}\isanewline
-\ \ \ \ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
 %
@@ -306,8 +281,7 @@
 \isamarkuptrue%
 \isacommand{interpretation}\isamarkupfalse%
 \ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
@@ -338,10 +312,6 @@
 \ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharparenright}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline
@@ -408,14 +378,7 @@
 \isacommand{interpretation}\isamarkupfalse%
 \ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline
 \ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}distrib{\isacharunderscore}lattice\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \isacommand{apply}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales%
 \begin{isamarkuptxt}%
 \begin{isabelle}%
@@ -426,7 +389,7 @@
 \end{isabelle}%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \isacommand{apply}\isamarkupfalse%
 \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharparenright}%
 \begin{isamarkuptxt}%
 \begin{isabelle}%
@@ -434,12 +397,9 @@
 \end{isabelle}%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}rule\ gcd{\isacharunderscore}lcm{\isacharunderscore}distr{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{done}\isamarkupfalse%
-\isanewline
-\isacommand{qed}\isamarkupfalse%
-\ {\isacharparenleft}rule\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharparenright}{\isacharplus}%
+\ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}rule\ gcd{\isacharunderscore}lcm{\isacharunderscore}distr{\isacharparenright}\ \isacommand{done}\isamarkupfalse%
+%
 \endisatagvisible
 {\isafoldvisible}%
 %
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/Main/Docs/document/Main_Doc.tex
--- a/doc-src/Main/Docs/document/Main_Doc.tex	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/Main/Docs/document/Main_Doc.tex	Thu Oct 01 20:20:56 2009 +0200
@@ -519,7 +519,7 @@
 \isa{takeWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
 \isa{tl} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
 \isa{upt} & \isa{nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\ list}\\
-\isa{upto} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
+\isa{upto} & \isa{int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ list}\\
 \isa{zip} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list}\\
 \end{supertabular}
 
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/System/Thy/ROOT.ML
--- a/doc-src/System/Thy/ROOT.ML	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/System/Thy/ROOT.ML	Thu Oct 01 20:20:56 2009 +0200
@@ -1,7 +1,4 @@
-set ThyOutput.source;
+Unsynchronized.set ThyOutput.source;
 use "../../antiquote_setup.ML";
 
-use_thy "Basics";
-use_thy "Interfaces";
-use_thy "Presentation";
-use_thy "Misc";
+use_thys ["Basics", "Interfaces", "Presentation", "Misc"];
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/TutorialI/Inductive/document/Advanced.tex
--- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Thu Oct 01 20:20:56 2009 +0200
@@ -362,7 +362,7 @@
 subgoal may look uninviting, but fortunately 
 \isa{lists} distributes over intersection:
 \begin{isabelle}%
-lists\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ lists\ A\ {\isasyminter}\ lists\ B\rulename{lists{\isacharunderscore}Int{\isacharunderscore}eq}%
+listsp\ {\isacharparenleft}{\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isasymin}\ A{\isacharparenright}\ {\isasyminter}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isasymin}\ B{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isasymin}\ lists\ A{\isacharparenright}\ {\isasyminter}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isasymin}\ lists\ B{\isacharparenright}\rulename{lists{\isacharunderscore}Int{\isacharunderscore}eq}%
 \end{isabelle}
 Thanks to this default simplification rule, the induction hypothesis 
 is quickly replaced by its two parts:
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Thu Oct 01 20:20:56 2009 +0200
@@ -17,7 +17,7 @@
 SRC = $(ISABELLE_HOME)/src
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
-OPTIONS = -m brackets -i true -d "" -D document
+OPTIONS = -m brackets -i true -d "" -D document -M 1
 USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS) $(OUT)/HOL
 
 
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/TutorialI/Misc/Itrev.thy
--- a/doc-src/TutorialI/Misc/Itrev.thy	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Thu Oct 01 20:20:56 2009 +0200
@@ -2,7 +2,7 @@
 theory Itrev
 imports Main
 begin
-ML"reset NameSpace.unique_names"
+ML"Unsynchronized.reset NameSpace.unique_names"
 (*>*)
 
 section{*Induction Heuristics*}
@@ -141,6 +141,6 @@
 \index{induction heuristics|)}
 *}
 (*<*)
-ML"set NameSpace.unique_names"
+ML"Unsynchronized.set NameSpace.unique_names"
 end
 (*>*)
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/TutorialI/Rules/Basic.thy
--- a/doc-src/TutorialI/Rules/Basic.thy	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy	Thu Oct 01 20:20:56 2009 +0200
@@ -188,7 +188,7 @@
 
 text{*unification failure trace *}
 
-ML "set trace_unify_fail"
+ML "Unsynchronized.set trace_unify_fail"
 
 lemma "P(a, f(b, g(e,a), b), a) \<Longrightarrow> P(a, f(b, g(c,a), b), a)"
 txt{*
@@ -213,7 +213,7 @@
 *}
 oops
 
-ML "reset trace_unify_fail"
+ML "Unsynchronized.reset trace_unify_fail"
 
 
 text{*Quantifiers*}
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy	Thu Oct 01 20:20:56 2009 +0200
@@ -1,7 +1,7 @@
 (* ID:         $Id$ *)
 theory Examples imports Main Binomial begin
 
-ML "reset eta_contract"
+ML "Unsynchronized.reset eta_contract"
 ML "Pretty.setmargin 64"
 
 text{*membership, intersection *}
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Thu Oct 01 20:20:56 2009 +0200
@@ -252,18 +252,13 @@
 \rulename{mult_cancel_left}
 *}
 
-ML{*set show_sorts*}
-
 text{*
 effect of show sorts on the above
 
-@{thm[display] mult_cancel_left[no_vars]}
+@{thm[display,show_sorts] mult_cancel_left[no_vars]}
 \rulename{mult_cancel_left}
 *}
 
-ML{*reset show_sorts*}
-
-
 text{*
 absolute value
 
diff -r 4602cb6ae0b5 -r 3a2fa964ad08 doc-src/TutorialI/Types/document/Numbers.tex
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Thu Oct 01 13:32:03 2009 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Thu Oct 01 20:20:56 2009 +0200
@@ -550,44 +550,18 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-\isacommand{ML}\isamarkupfalse%
-{\isacharverbatimopen}set\ show{\isacharunderscore}sorts{\isacharverbatimclose}%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
 \begin{isamarkuptext}%
 effect of show sorts on the above
 
 \begin{isabelle}%
-{\isacharparenleft}c\ {\isacharasterisk}\ a\ {\isacharequal}\ c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
+{\isacharparenleft}{\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharequal}\isanewline
+\isaindent{{\isacharparenleft}}c\ {\isacharasterisk}\ {\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+{\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
 \end{isabelle}
 \rulename{mult_cancel_left}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-\isacommand{ML}\isamarkupfalse%
-{\isacharverbatimopen}reset\ show{\isacharunderscore}sorts{\isacharverbatimclose}%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
 \begin{isamarkuptext}%
 absolute value