# HG changeset patch
# User wenzelm
# Date 1254420371 -7200
# Node ID a4e0b8d88f28d7dac5938d9bc45fffde471d9b0c
# Parent  f3716d1a2e48a948755d0567f98017ebaf5fa6e1
avoid unsynchronized refs within theory sources;

diff -r f3716d1a2e48 -r a4e0b8d88f28 doc-src/IsarOverview/Isar/Logic.thy
--- a/doc-src/IsarOverview/Isar/Logic.thy	Thu Oct 01 20:04:44 2009 +0200
+++ b/doc-src/IsarOverview/Isar/Logic.thy	Thu Oct 01 20:06:11 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 f3716d1a2e48 -r a4e0b8d88f28 doc-src/IsarOverview/Isar/ROOT.ML
--- a/doc-src/IsarOverview/Isar/ROOT.ML	Thu Oct 01 20:04:44 2009 +0200
+++ b/doc-src/IsarOverview/Isar/ROOT.ML	Thu Oct 01 20:06:11 2009 +0200
@@ -1,2 +1,3 @@
-use_thy "Logic";
-use_thy "Induction"
+Unsynchronized.set quick_and_dirty;
+
+use_thys ["Logic", "Induction"];
diff -r f3716d1a2e48 -r a4e0b8d88f28 doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Thu Oct 01 20:04:44 2009 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Thu Oct 01 20:06:11 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