Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Minor proof tuning.
authorwebertj
Sun, 23 May 2010 14:56:58 +0100
changeset 37092 891d3333ead1
parent 37091 088ad0b57137
child 37093 8808a1aa12a2
Minor proof tuning.
src/HOL/Library/Kleene_Algebra.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Kleene_Algebra.thy	Sun May 23 13:00:01 2010 +0100
+++ b/src/HOL/Library/Kleene_Algebra.thy	Sun May 23 14:56:58 2010 +0100
@@ -232,7 +232,7 @@
   thus "x + star b * x * a \<le> x + star b * b * x"
     using add_mono by auto
   show "\<dots> \<le> star b * x"
-    by (metis add_supremum left_distrib less_add mult.left_neutral mult_assoc mult_right_mono star_unfold_left star_unfold_right zero_minimum)
+    by (metis add_supremum left_distrib less_add mult.left_neutral mult_assoc mult_right_mono star_unfold_right zero_minimum)
 qed
 
 lemma star_simulation [simp]:
isabelle