src/HOL/Presburger.thy
changeset 49962 a8cc904a6820
parent 48891 c0eafbd55de3
child 54227 63b441f49645
     1.1 --- a/src/HOL/Presburger.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4    "(d::'a::{comm_ring,Rings.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
     1.5    "\<forall>x k. F = F"
     1.6  apply (auto elim!: dvdE simp add: algebra_simps)
     1.7 -unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric]
     1.8 +unfolding mult_assoc [symmetric] distrib_right [symmetric] left_diff_distrib [symmetric]
     1.9  unfolding dvd_def mult_commute [of d] 
    1.10  by auto
    1.11