--- a/IntEx.thy	Fri Nov 13 19:32:12 2009 +0100
+++ b/IntEx.thy	Wed Nov 18 23:52:48 2009 +0100
@@ -20,16 +20,23 @@
 where
   "ZERO \<equiv> (0::nat, 0::nat)"
 
+ML {* print_qconstinfo @{context} *}
+
+
 term ZERO
 thm ZERO_def
 
 ML {* prop_of @{thm ZERO_def} *}
 
+ML {* separate *}
+
 quotient_def 
   ONE::"my_int"
 where
   "ONE \<equiv> (1::nat, 0::nat)"
 
+ML {* print_qconstinfo @{context} *}
+
 term ONE
 thm ONE_def
 
@@ -43,6 +50,7 @@
 where
   "PLUS \<equiv> my_plus"
 
+term my_plus
 term PLUS
 thm PLUS_def