diff -r d3c7f6d19c7f -r 746b17e1d6d8 IntEx.thy --- 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 \ (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 \ (1::nat, 0::nat)" +ML {* print_qconstinfo @{context} *} + term ONE thm ONE_def @@ -43,6 +50,7 @@ where "PLUS \ my_plus" +term my_plus term PLUS thm PLUS_def