--- a/IntEx.thy	Wed Oct 28 10:29:00 2009 +0100
+++ b/IntEx.thy	Wed Oct 28 15:25:11 2009 +0100
@@ -12,27 +12,17 @@
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
-print_quotients
-
-typ my_int
+quotient_def (for my_int)
+  ZERO::"my_int"
+where
+  "ZERO \<equiv> (0::nat, 0::nat)"
 
-local_setup {*
-  make_const_def @{binding "ZERO"} @{term "(0::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
-*}
-
-term ZERO
 thm ZERO_def
 
-(*
-quotient_def (with my_int)
-  ZERO :: "my_int"
+quotient_def (for my_int)
+  ONE::"my_int"
 where
-  "ZERO \<equiv> (0::nat, 0::nat)"
-*)
-
-local_setup {*
-  make_const_def @{binding ONE} @{term "(1::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
-*}
+  "ONE \<equiv> (1::nat, 0::nat)"
 
 term ONE
 thm ONE_def
@@ -42,9 +32,10 @@
 where
   "my_plus (x, y) (u, v) = (x + u, y + v)"
 
-local_setup {*
-  make_const_def @{binding PLUS} @{term "my_plus"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
-*}
+quotient_def (for my_int)
+  PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+where
+  "PLUS \<equiv> my_plus"
 
 term PLUS
 thm PLUS_def
@@ -55,7 +46,7 @@
   "my_neg (x, y) = (y, x)"
 
 local_setup {*
-  make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
+  old_make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
 *}
 
 term NEG
@@ -72,7 +63,7 @@
   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
 local_setup {*
-  make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
+  old_make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
 *}
 
 term MULT
@@ -85,7 +76,7 @@
   "my_le (x, y) (u, v) = (x+v \<le> u+y)"
 
 local_setup {*
-  make_const_def @{binding LE} @{term "my_le"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
+  old_make_const_def @{binding LE} @{term "my_le"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
 *}
 
 term LE