--- a/IntEx.thy	Wed Nov 11 22:30:43 2009 +0100
+++ b/IntEx.thy	Thu Nov 12 02:18:36 2009 +0100
@@ -109,6 +109,10 @@
 where
  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
+ML {* print_qconstinfo @{context} *}
+
+ML {* print_qconstinfo @{context} *}
+
 lemma plus_sym_pre:
   shows "my_plus a b \<approx> my_plus b a"
   apply(cases a)