| changeset 35028 | 108662d50512 |
| parent 32238 | 74ae5e9f312c |
| child 37088 | 36c13099d10f |
--- a/src/HOL/Library/Kleene_Algebra.thy Fri Feb 05 14:33:31 2010 +0100 +++ b/src/HOL/Library/Kleene_Algebra.thy Fri Feb 05 14:33:50 2010 +0100 @@ -72,7 +72,7 @@ class pre_kleene = semiring_1 + order_by_add begin -subclass pordered_semiring proof +subclass ordered_semiring proof fix x y z :: 'a assume "x \<le> y"