--- a/doc-src/Locales/Locales/Examples3.thy Mon Jan 19 21:20:18 2009 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy Mon Jan 19 23:40:29 2009 +0100
@@ -178,8 +178,6 @@
nat_dvd_join_eq} are named since they are handy in the proof of
the subsequent interpretation. *}
-ML %invisible {* set quick_and_dirty *}
-
(*
definition
is_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
@@ -200,8 +198,6 @@
lemma %invisible gcd_lcm_distr:
"gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry
-ML %invisible {* reset quick_and_dirty *}
-
interpretation %visible nat_dvd:
distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
apply unfold_locales
--- a/doc-src/Locales/Locales/ROOT.ML Mon Jan 19 21:20:18 2009 +0100
+++ b/doc-src/Locales/Locales/ROOT.ML Mon Jan 19 23:40:29 2009 +0100
@@ -1,4 +1,4 @@
no_document use_thy "GCD";
use_thy "Examples1";
use_thy "Examples2";
-use_thy "Examples3";
+setmp_noncritical quick_and_dirty true use_thy "Examples3";
--- a/doc-src/Locales/Locales/document/Examples3.tex Mon Jan 19 21:20:18 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex Mon Jan 19 23:40:29 2009 +0100
@@ -362,18 +362,10 @@
\endisadeliminvisible
%
\isataginvisible
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\ set\ quick{\isacharunderscore}and{\isacharunderscore}dirty\ {\isacharverbatimclose}\isanewline
-\isanewline
-\isanewline
-\isanewline
\isacommand{lemma}\isamarkupfalse%
\ gcd{\isacharunderscore}lcm{\isacharunderscore}distr{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}gcd\ x\ {\isacharparenleft}lcm\ y\ z{\isacharparenright}\ {\isacharequal}\ lcm\ {\isacharparenleft}gcd\ x\ y{\isacharparenright}\ {\isacharparenleft}gcd\ x\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\ reset\ quick{\isacharunderscore}and{\isacharunderscore}dirty\ {\isacharverbatimclose}%
+%
\endisataginvisible
{\isafoldinvisible}%
%
@@ -383,7 +375,7 @@
\isanewline
%
\isadelimvisible
-\ \ \isanewline
+\isanewline
%
\endisadelimvisible
%