src/HOL/Library/Saturated.thy
changeset 44848 f4d0b060c7ca
parent 44819 fe33d6655186
child 44849 41fddafe20d5
     1.1 --- a/src/HOL/Library/Saturated.thy	Thu Sep 08 18:13:48 2011 -0700
     1.2 +++ b/src/HOL/Library/Saturated.thy	Thu Sep 08 18:47:23 2011 -0700
     1.3 @@ -131,7 +131,7 @@
     1.4      case True thus ?thesis by (simp add: sat_eq_iff)
     1.5    next
     1.6      case False thus ?thesis
     1.7 -      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)
     1.8 +      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)
     1.9    qed
    1.10  qed (simp_all add: sat_eq_iff mult.commute)
    1.11