src/HOL/Presburger.thy
changeset 23438 dd824e86fa8a
parent 23430 771117253634
child 23460 f9ae34d5f8da
     1.1 --- a/src/HOL/Presburger.thy	Wed Jun 20 17:02:57 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Wed Jun 20 17:28:55 2007 +0200
     1.3 @@ -389,7 +389,7 @@
     1.4  
     1.5  lemma zdiff_int_split: "P (int (x - y)) =
     1.6    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
     1.7 -  by (case_tac "y \<le> x", simp_all)
     1.8 +  by (case_tac "y \<le> x", simp_all add: zdiff_int)
     1.9  
    1.10  lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
    1.11  lemma number_of2: "(0::int) <= Numeral0" by simp