# HG changeset patch # User haftmann # Date 1232027543 -3600 # Node ID b19b8793b71c27f307befb79fd65f4fae83d1234 # Parent ec072307c69bd8e527bb09a981384f37eaa18127 decativate Toplevel.debug after reading diff -r ec072307c69b -r b19b8793b71c 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