--- a/src/HOL/Algebra/abstract/Ideal2.thy Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ideal2.thy Sun Mar 21 17:12:31 2010 +0100
@@ -1,9 +1,11 @@
-(*
- Ideals for commutative rings
- Author: Clemens Ballarin, started 24 September 1999
+(* Author: Clemens Ballarin, started 24 September 1999
+
+Ideals for commutative rings.
*)
-theory Ideal2 imports Ring2 begin
+theory Ideal2
+imports Ring2
+begin
definition
is_ideal :: "('a::ring) set => bool" where
@@ -28,8 +30,8 @@
(* is_ideal *)
lemma is_idealI:
- "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;
- !! a. a:I ==> - a : I; 0 : I;
+ "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;
+ !! a. a:I ==> - a : I; 0 : I;
!! a r. a:I ==> a * r : I |] ==> is_ideal I"
unfolding is_ideal_def by blast
@@ -241,7 +243,7 @@
apply force
done
-lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]
+lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]
==> is_ideal (Union (I`UNIV))"
apply (rule is_idealI)
apply auto