Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Saturated.thy
changeset 44848 f4d0b060c7ca
parent 44819 fe33d6655186
child 44849 41fddafe20d5 
--- a/src/HOL/Library/Saturated.thy	Thu Sep 08 18:13:48 2011 -0700
+++ b/src/HOL/Library/Saturated.thy	Thu Sep 08 18:47:23 2011 -0700
@@ -131,7 +131,7 @@
     case True thus ?thesis by (simp add: sat_eq_iff)
   next
     case False thus ?thesis
-      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib nat_add_min_left nat_add_min_right min_max.inf_assoc min_max.inf_absorb2)
+      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min_max.inf_assoc min_max.inf_absorb2)
   qed
 qed (simp_all add: sat_eq_iff mult.commute)
isabelle