diff -r 93c9022ba5e9 -r c4001cda9da3 Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/IntEx2.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -21,10 +21,10 @@
 ML {* @{term "0 \<Colon> int"} *}
 
 quotient_definition
-  "0 \<Colon> int" as "(0\<Colon>nat, 0\<Colon>nat)"
+  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
 
 quotient_definition
-  "1 \<Colon> int" as "(1\<Colon>nat, 0\<Colon>nat)"
+  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
 
 fun
   plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -32,7 +32,7 @@
   "plus_raw (x, y) (u, v) = (x + u, y + v)"
 
 quotient_definition
-  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw"
+  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_raw"
 
 fun
   uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -40,7 +40,7 @@
   "uminus_raw (x, y) = (y, x)"
 
 quotient_definition
-  "(uminus \<Colon> (int \<Rightarrow> int))" as "uminus_raw"
+  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_raw"
 
 definition
   minus_int_def [code del]:  "z - w = z + (-w\<Colon>int)"
@@ -51,7 +51,7 @@
   "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
 quotient_definition
-  mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "mult_raw"
+  mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "mult_raw"
 
 fun
   le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
@@ -59,7 +59,7 @@
   "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
 quotient_definition
-  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "le_raw"
+  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_raw"
 
 definition
   less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
@@ -207,7 +207,7 @@
   "int_of_nat_raw m = (m :: nat, 0 :: nat)"
 
 quotient_definition
-  "int_of_nat :: nat \<Rightarrow> int" as "int_of_nat_raw"
+  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
 
 lemma[quot_respect]: 
   shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"