diff -r dd4d05587bd0 -r 10a6ba364ce1 Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Thu Feb 11 17:58:06 2010 +0100
+++ b/Quot/Examples/IntEx2.thy	Fri Feb 12 12:06:09 2010 +0100
@@ -329,13 +329,6 @@
     by (simp only: zsgn_def)
 qed
 
-instance int :: linordered_ring
-proof  
-(*  fix k :: int
-  show "abs k = sup k (- k)"
-    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])*)
-qed
-
 lemmas int_distrib =
   left_distrib [of "z1::int" "z2" "w", standard]
   right_distrib [of "w::int" "z1" "z2", standard]