src/HOL/Integ/Presburger.thy
 changeset 17589 58eeffd73be1 parent 17378 105519771c67 child 18202 46af82efd311
```     1.1 --- a/src/HOL/Integ/Presburger.thy	Thu Sep 22 23:55:42 2005 +0200
1.2 +++ b/src/HOL/Integ/Presburger.thy	Thu Sep 22 23:56:15 2005 +0200
1.3 @@ -244,10 +244,10 @@
1.4  text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
1.5
1.6  lemma P_eqtrue: "(P=True) = P"
1.7 -  by rules
1.8 +  by iprover
1.9
1.10  lemma P_eqfalse: "(P=False) = (~P)"
1.11 -  by rules
1.12 +  by iprover
1.13
1.14  text {*
1.15    \medskip Theorems for the generation of the bachwards direction of
1.16 @@ -831,10 +831,10 @@
1.17    by simp
1.18
1.19  lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
1.20 -  by rules
1.21 +  by iprover
1.22
1.23  lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
1.24 -  by rules
1.25 +  by iprover
1.26
1.27  lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
1.28  ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
1.29 @@ -952,13 +952,13 @@
1.30    apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
1.32    apply (rule iffI)
1.33 -  apply rules
1.34 +  apply iprover
1.35    apply (erule exE)
1.36    apply (case_tac "x=0")
1.37    apply (rule_tac x=0 in exI)
1.38    apply simp
1.39    apply (case_tac "0 \<le> k")
1.40 -  apply rules
1.41 +  apply iprover