src/HOL/Library/Kleene_Algebra.thy

--- a/src/HOL/Library/Kleene_Algebra.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Library/Kleene_Algebra.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -367,7 +367,7 @@
 
 class kleene_by_complete_lattice = pre_kleene
   + complete_lattice + power + star +
-  assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
+  assumes star_cont: "a * star b * c = SUPREMUM UNIV (\<lambda>n. a * b ^ n * c)"
 begin
 
 subclass kleene