diff -r 6decb8811d30 -r 587e97d144a0 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Fri Dec 11 11:12:53 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Fri Dec 11 11:14:05 2009 +0100
@@ -22,13 +22,13 @@
 print_quotients
 
 quotient_def
-  ZERO::"zero :: my_int"
-where
+  "ZERO :: my_int"
+as
   "(0::nat, 0::nat)"
 
 quotient_def
-  ONE::"one :: my_int"
-where
+  "ONE :: my_int"
+as
   "(1::nat, 0::nat)"
 
 fun
@@ -37,8 +37,8 @@
   "my_plus (x, y) (u, v) = (x + u, y + v)"
 
 quotient_def
-  PLUS::"PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-where
+  "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+as
   "my_plus"
 
 fun
@@ -47,8 +47,8 @@
   "my_neg (x, y) = (y, x)"
 
 quotient_def
-  NEG::"NEG :: my_int \<Rightarrow> my_int"
-where
+  "NEG :: my_int \<Rightarrow> my_int"
+as
   "my_neg"
 
 definition
@@ -62,8 +62,8 @@
   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
 quotient_def
-  MULT::"MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-where
+  "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+as
   "my_mult"
 
 
@@ -74,8 +74,8 @@
   "my_le (x, y) (u, v) = (x+v \<le> u+y)"
 
 quotient_def
-  LE :: "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
-where
+   "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
+as
   "my_le"
 
 term LE