changeset 22473 | 753123c89d72 |
parent 22459 | 8469640e1489 |
child 22665 | cf152ff55d16 |
--- a/src/HOL/Library/Kleene_Algebras.thy Mon Mar 19 19:28:27 2007 +0100 +++ b/src/HOL/Library/Kleene_Algebras.thy Tue Mar 20 08:27:15 2007 +0100 @@ -9,7 +9,7 @@ text {* A type class of kleene algebras *} -class star = +class star = type + fixes star :: "'a \<Rightarrow> 'a" class idem_add = ab_semigroup_add +