src/HOL/Algebra/Ring.thy

   Id:        $Id$
   Author:    Clemens Ballarin, started 9 December 1996
   Copyright: Clemens Ballarin
 *)
 
-theory Ring imports FiniteProduct
+theory Ring
+imports FiniteProduct
 uses ("ringsimp.ML") begin
 
 
 section {* The Algebraic Hierarchy of Rings *}
 

   assumes cg: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   shows "abelian_group G"
 proof -
   interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
     by (rule cg)
-  show "abelian_group G" by (unfold_locales)
+  show "abelian_group G" ..
 qed
 
 
 subsection {* Sums over Finite Sets *}
 

   by (auto intro: ring.intro
     abelian_group.axioms ring_axioms.intro assms)
 
 lemma (in ring) is_abelian_group:
   "abelian_group R"
-  by unfold_locales
+  ..
 
 lemma (in ring) is_monoid:
   "monoid R"
   by (auto intro!: monoidI m_assoc)
 

 text {* Field would not need to be derived from domain, the properties
   for domain follow from the assumptions of field *}
 lemma (in cring) cring_fieldI:
   assumes field_Units: "Units R = carrier R - {\<zero>}"
   shows "field R"
-proof unfold_locales
+proof
   from field_Units
   have a: "\<zero> \<notin> Units R" by fast
   have "\<one> \<in> Units R" by fast
   from this and a
   show "\<one> \<noteq> \<zero>" by force