dropped print_interps
authorhaftmann
Wed, 21 Jan 2009 18:37:44 +0100
changeset 29586 4f9803829625
parent 29585 c23295521af5
child 29600 0182b65e4ad0
child 29601 93553f7c722f
child 29608 564ea783ace8
dropped print_interps
src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Wed Jan 21 18:27:43 2009 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Wed Jan 21 18:37:44 2009 +0100
@@ -625,9 +625,6 @@
 lemma "gcd x y dvd x"
   apply (rule nat_dvd.meet_left) done
 
-print_interps dpo
-print_interps dlat
-
 
 subsection {* Group example with defined operations @{text inv} and @{text unit} *}