src/HOL/ex/LocaleTest2.thy
changeset 29586 4f9803829625
parent 29233 ce6d35a0bed6
child 30729 461ee3e49ad3
--- 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} *}