diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/IntEx2.thy	Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
 theory IntEx2
-imports "../QuotMain" "../QuotProd" Nat
+imports "../Quotient" "../Quotient_Product" Nat
 (*uses
   ("Tools/numeral.ML")
   ("Tools/numeral_syntax.ML")
@@ -271,7 +271,7 @@
 by (cases i, cases j, cases k) (simp)
 
 
-instance int :: pordered_cancel_ab_semigroup_add
+instance int :: ordered_cancel_ab_semigroup_add
 proof
   fix i j k :: int
   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
@@ -318,7 +318,7 @@
 done
 
 text{*The integers form an ordered integral domain*}
-instance int :: ordered_idom
+instance int :: linordered_idom
 proof
   fix i j k :: int
   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
@@ -329,11 +329,11 @@
     by (simp only: zsgn_def)
 qed
 
-instance int :: lordered_ring
+instance int :: linordered_ring
 proof  
-  fix k :: int
+(*  fix k :: int
   show "abs k = sup k (- k)"
-    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
+    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])*)
 qed
 
 lemmas int_distrib =