diff -r add8f7f311cd -r 810d59a3d9b0 Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Fri Dec 11 11:25:52 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Fri Dec 11 11:30:00 2009 +0100
@@ -18,13 +18,13 @@
 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
 begin
 
-ML {* @{term "0 :: int"} *}
+ML {* @{term "0 \<Colon> int"} *}
 
 quotient_def
-  "0 :: int" as "(0::nat, 0::nat)"
+  "0 \<Colon> int" as "(0\<Colon>nat, 0\<Colon>nat)"
 
 quotient_def
-  "1 :: int" as "(1::nat, 0::nat)"
+  "1 \<Colon> int" as "(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_def
-  "(op +) :: (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw"
+  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw"
 
 fun
   uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -40,10 +40,10 @@
   "uminus_raw (x, y) = (y, x)"
 
 quotient_def
-  "(uminus :: (int \<Rightarrow> int))" as "uminus_raw"
+  "(uminus \<Colon> (int \<Rightarrow> int))" as "uminus_raw"
 
 definition
-  minus_int_def [code del]:  "z - w = z + (-w::int)"
+  minus_int_def [code del]:  "z - w = z + (-w\<Colon>int)"
 
 fun
   mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -65,10 +65,10 @@
   less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
 
 definition
-  abs_int_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
 
 definition
-  sgn_int_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
+  zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
 
 instance ..
 
@@ -324,16 +324,16 @@
   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
     by (rule zmult_zless_mono2)
   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
-    by (simp only: abs_int_def)
+    by (simp only: zabs_def)
   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
-    by (simp only: sgn_int_def)
+    by (simp only: zsgn_def)
 qed
 
 instance int :: lordered_ring
 proof  
   fix k :: int
   show "abs k = sup k (- k)"
-    by (auto simp add: sup_int_def abs_int_def less_minus_self_iff [symmetric])
+    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
 qed
 
 lemmas int_distrib =