diff -r 6decb8811d30 -r 587e97d144a0 Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Fri Dec 11 11:12:53 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Fri Dec 11 11:14:05 2009 +0100
@@ -18,15 +18,13 @@
 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
 begin
 
-quotient_def
-  zero_int::"0 :: int"
-where
-  "(0::nat, 0::nat)"
+ML {* @{term "0 :: int"} *}
 
 quotient_def
-  one_int::"1 :: int"
-where
-  "(1::nat, 0::nat)"
+  "0 :: int" as "(0::nat, 0::nat)"
+
+quotient_def
+  "1 :: int" as "(1::nat, 0::nat)"
 
 fun
   plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -34,9 +32,7 @@
   "plus_raw (x, y) (u, v) = (x + u, y + v)"
 
 quotient_def
-  plus_int::"(op +) :: (int \<Rightarrow> int \<Rightarrow> int)"
-where
-  "plus_raw"
+  "(op +) :: (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw"
 
 fun
   uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -44,9 +40,7 @@
   "uminus_raw (x, y) = (y, x)"
 
 quotient_def
-  uminus_int::"(uminus :: (int \<Rightarrow> int))"
-where
-  "uminus_raw"
+  "(uminus :: (int \<Rightarrow> int))" as "uminus_raw"
 
 definition
   minus_int_def [code del]:  "z - w = z + (-w::int)"
@@ -57,9 +51,7 @@
   "times_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
 quotient_def
-  times_int::"(op *) :: (int \<Rightarrow> int \<Rightarrow> int)"
-where
-  "times_raw"
+  "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "times_raw"
 
 (* PROBLEM: this should be called le_int and le_raw / or odd *)
 fun
@@ -68,9 +60,7 @@
   "less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
 quotient_def
-  less_eq_int :: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
-where
-  "less_eq_raw"
+  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "less_eq_raw"
 
 definition
   less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
@@ -218,8 +208,7 @@
   "int_of_nat_raw m = (m :: nat, 0 :: nat)"
 
 quotient_def
-  int_of_nat :: "int_of_nat :: nat \<Rightarrow> int" 
-where "int_of_nat_raw"
+  "int_of_nat :: nat \<Rightarrow> int" as "int_of_nat_raw"
 
 lemma[quot_respect]: 
   shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"