decativate Toplevel.debug after reading
authorhaftmann
Thu, 15 Jan 2009 14:52:23 +0100
changeset 29492 b19b8793b71c
parent 29485 ec072307c69b
child 29493 ddcbd5e4041d
decativate Toplevel.debug after reading
src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Wed Jan 14 13:47:14 2009 -0800
+++ b/src/FOL/ex/LocaleTest.thy	Thu Jan 15 14:52:23 2009 +0100
@@ -1,7 +1,7 @@
 (*  Title:      FOL/ex/NewLocaleTest.thy
     Author:     Clemens Ballarin, TU Muenchen
 
-Testing environment for locale expressions --- experimental.
+Testing environment for locale expressions.
 *)
 
 theory LocaleTest
@@ -483,4 +483,6 @@
   thm local_free.lone [where ?zero = 0]
 qed
 
+ML_val {* reset Toplevel.debug *}
+
 end