src/HOL/Algebra/IntRing.thy

   Id:        $Id$
   Author:    Stephan Hohe, TU Muenchen
 *)
 
 theory IntRing
-imports QuotRing Int Primes
+imports QuotRing Lattice Int Primes
 begin
 
 
 section {* The Ring of Integers *}
 

     and "mult \<Z> x y = x * y"
     and "one \<Z> = 1"
     and "pow \<Z> x n = x^n"
 proof -
   -- "Specification"
-  show "monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
+  show "monoid \<Z>" proof qed (auto simp: int_ring_def)
   then interpret int: monoid ["\<Z>"] .
 
   -- "Carrier"
   show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
 

 
 interpretation int: comm_monoid ["\<Z>"]
   where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
 proof -
   -- "Specification"
-  show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
+  show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
   then interpret int: comm_monoid ["\<Z>"] .
 
   -- "Operations"
   { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
   note mult = this

   where "zero \<Z> = 0"
     and "add \<Z> x y = x + y"
     and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
 proof -
   -- "Specification"
-  show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
+  show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
   then interpret int: abelian_monoid ["\<Z>"] .
 
   -- "Operations"
   { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
   note add = this

   note a_inv = this
   show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
 qed
 
 interpretation int: "domain" ["\<Z>"]
-  by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)
+  proof qed (auto simp: int_ring_def left_distrib right_distrib)
 
 
 text {* Removal of occurrences of @{term UNIV} in interpretation result
   --- experimental. *}
 

   where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
     and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
     and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
 proof -
   show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
-    by unfold_locales simp_all
+    proof qed simp_all
   show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
     by simp
   show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
     by simp
   show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"

     done
 qed
 
 interpretation int (* [unfolded UNIV] *) :
   total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
-  by unfold_locales clarsimp
+  proof qed clarsimp
 
 
 subsection {* Generated Ideals of @{text "\<Z>"} *}
 
 lemma int_Idl: