diff -r ab8a58973861 -r cc951743c5e2 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Thu Jan 14 12:23:59 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Jan 14 15:25:24 2010 +0100
@@ -13,15 +13,6 @@
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
-thm quot_equiv
-
-thm quot_thm
-
-thm my_int_equivp
-
-print_theorems
-print_quotients
-
 quotient_definition
   "ZERO :: my_int"
 as