# HG changeset patch
# User ballarin
# Date 1071062945 -3600
# Node ID 0ae66ffb978421313bdcb5dcde8fdae52f54e46c
# Parent  92ed032e83a1f4babe49aa54d7faf450874275f4
New structure "partial_object" as common root for lattices and magmas.

diff -r 92ed032e83a1 -r 0ae66ffb9784 src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Wed Dec 10 14:27:50 2003 +0100
+++ b/src/HOL/Algebra/CRing.thy	Wed Dec 10 14:29:05 2003 +0100
@@ -90,7 +90,7 @@
   by (unfold comm_semigroup_def semigroup_def)
     (fast intro: comm_monoid.axioms a_comm_monoid)
 
-lemmas monoid_record_simps = semigroup.simps monoid.simps
+lemmas monoid_record_simps = partial_object.simps semigroup.simps monoid.simps
 
 lemma (in abelian_monoid) a_closed [intro, simp]:
   "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y \<in> carrier G"
diff -r 92ed032e83a1 -r 0ae66ffb9784 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Dec 10 14:27:50 2003 +0100
+++ b/src/HOL/Algebra/Group.thy	Wed Dec 10 14:29:05 2003 +0100
@@ -20,8 +20,12 @@
 
 subsection {* Definitions *}
 
-record 'a semigroup =
+(* Object with a carrier set. *)
+
+record 'a partial_object =
   carrier :: "'a set"
+
+record 'a semigroup = "'a partial_object" +
   mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
 
 record 'a monoid = "'a semigroup" +