--- a/src/HOL/Algebra/Ring.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Ring.thy Mon Nov 17 17:00:55 2008 +0100
@@ -5,7 +5,8 @@
Copyright: Clemens Ballarin
*)
-theory Ring imports FiniteProduct
+theory Ring
+imports FiniteProduct
uses ("ringsimp.ML") begin
@@ -188,7 +189,7 @@
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
@@ -392,7 +393,7 @@
lemma (in ring) is_abelian_group:
"abelian_group R"
- by unfold_locales
+ ..
lemma (in ring) is_monoid:
"monoid R"
@@ -670,7 +671,7 @@
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