# HG changeset patch
# User wenzelm
# Date 1232404829 -3600
# Node ID ba144750086d4424c371b795c681adcb51dcb67b
# Parent  286c01be90cb74ac8f7f174f5bc34c7aed9a764c
more robust handling of quick_and_dirty;

diff -r 286c01be90cb -r ba144750086d doc-src/Locales/Locales/Examples3.thy
--- 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
diff -r 286c01be90cb -r ba144750086d doc-src/Locales/Locales/ROOT.ML
--- 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";
diff -r 286c01be90cb -r ba144750086d doc-src/Locales/Locales/document/Examples3.tex
--- 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
 %