diff -r 93c9022ba5e9 -r c4001cda9da3 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -15,12 +15,12 @@
 
 quotient_definition
   "ZERO :: my_int"
-as
+is
   "(0::nat, 0::nat)"
 
 quotient_definition
   "ONE :: my_int"
-as
+is
   "(1::nat, 0::nat)"
 
 fun
@@ -30,7 +30,7 @@
 
 quotient_definition
   "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-as
+is
   "my_plus"
 
 fun
@@ -40,7 +40,7 @@
 
 quotient_definition
   "NEG :: my_int \<Rightarrow> my_int"
-as
+is
   "my_neg"
 
 definition
@@ -55,7 +55,7 @@
 
 quotient_definition
   "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-as
+is
   "my_mult"
 
 
@@ -67,7 +67,7 @@
 
 quotient_definition
    "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
-as
+is
   "my_le"
 
 term LE