--- a/IntEx.thy	Thu Nov 05 10:46:54 2009 +0100
+++ b/IntEx.thy	Thu Nov 05 13:47:04 2009 +0100
@@ -23,6 +23,8 @@
 term ZERO
 thm ZERO_def
 
+ML {* prop_of @{thm ZERO_def} *}
+
 quotient_def 
   ONE::"my_int"
 where
@@ -44,6 +46,10 @@
 term PLUS
 thm PLUS_def
 
+ML {* toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy"; *}
+
+ML {* prop_of @{thm PLUS_def} *}
+
 fun
   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where