diff -r 2d9de77d5687 -r 0dd10a900cae Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Wed Dec 09 15:57:47 2009 +0100
@@ -1,5 +1,5 @@
 theory IntEx
-imports "../QuotList" "../QuotProd" Nitpick
+imports "../QuotProd" "../QuotList"
 begin
 
 fun
@@ -21,56 +21,35 @@
 print_theorems
 print_quotients
 
-quotient_def 
-  ZERO::"my_int"
+quotient_def
+  ZERO::"zero :: my_int"
 where
-  "ZERO \<equiv> (0::nat, 0::nat)"
-
-ML {* print_qconstinfo @{context} *}
-
-term ZERO
-thm ZERO_def
-
-ML {* prop_of @{thm ZERO_def} *}
+  "(0::nat, 0::nat)"
 
-ML {* separate *}
-
-quotient_def 
-  ONE::"my_int"
+quotient_def
+  ONE::"one :: my_int"
 where
-  "ONE \<equiv> (1::nat, 0::nat)"
-
-ML {* print_qconstinfo @{context} *}
-
-term ONE
-thm ONE_def
+  "(1::nat, 0::nat)"
 
 fun
   my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
   "my_plus (x, y) (u, v) = (x + u, y + v)"
 
-quotient_def 
-  PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+quotient_def
+  PLUS::"PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 where
-  "PLUS \<equiv> my_plus"
-
-term my_plus
-term PLUS
-thm PLUS_def
+  "my_plus"
 
 fun
   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
   "my_neg (x, y) = (y, x)"
 
-quotient_def 
-  NEG::"my_int \<Rightarrow> my_int"
+quotient_def
+  NEG::"NEG :: my_int \<Rightarrow> my_int"
 where
-  "NEG \<equiv> my_neg"
-
-term NEG
-thm NEG_def
+  "my_neg"
 
 definition
   MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int"
@@ -82,13 +61,11 @@
 where
   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-quotient_def 
-  MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+quotient_def
+  MULT::"MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 where
-  "MULT \<equiv> my_mult"
+  "my_mult"
 
-term MULT
-thm MULT_def
 
 (* NOT SURE WETHER THIS DEFINITION IS CORRECT *)
 fun
@@ -96,10 +73,10 @@
 where
   "my_le (x, y) (u, v) = (x+v \<le> u+y)"
 
-quotient_def 
-  LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
+quotient_def
+  LE :: "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
 where
-  "LE \<equiv> my_le"
+  "my_le"
 
 term LE
 thm LE_def