diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Integ/Presburger.thy --- a/src/HOL/Integ/Presburger.thy Thu Sep 22 23:55:42 2005 +0200 +++ b/src/HOL/Integ/Presburger.thy Thu Sep 22 23:56:15 2005 +0200 @@ -244,10 +244,10 @@ text {* Theorems to be deleted from simpset when proving simplified formulaes. *} lemma P_eqtrue: "(P=True) = P" - by rules + by iprover lemma P_eqfalse: "(P=False) = (~P)" - by rules + by iprover text {* \medskip Theorems for the generation of the bachwards direction of @@ -831,10 +831,10 @@ by simp lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))" - by rules + by iprover lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))" - by rules + by iprover lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) " @@ -952,13 +952,13 @@ apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric] nat_0_le cong add: conj_cong) apply (rule iffI) - apply rules + apply iprover apply (erule exE) apply (case_tac "x=0") apply (rule_tac x=0 in exI) apply simp apply (case_tac "0 \ k") - apply rules + apply iprover apply (simp add: linorder_not_le) apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]]) apply assumption