diff -r 556ce89b7d41 -r af3b71a46a1c src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy Wed May 19 11:21:19 2004 +0200
+++ b/src/HOL/Integ/Presburger.thy Wed May 19 11:23:59 2004 +0200
@@ -978,11 +978,11 @@
\medskip Specific instances of congruence rules, to prevent
simplifier from looping. *}
-theorem imp_le_cong: "(0 <= x \ P = P') \ (0 <= (x::nat) \ P) = (0 <= x \ P')"
+theorem imp_le_cong: "(0 <= x \ P = P') \ (0 <= (x::int) \ P) = (0 <= x \ P')"
by simp
-theorem conj_le_cong: "(0 <= x \ P = P') \ (0 <= (x::nat) \ P) = (0 <= x \ P')"
- by simp
+theorem conj_le_cong: "(0 <= x \ P = P') \ (0 <= (x::int) \ P) = (0 <= x \ P')"
+ by (simp cong: conj_cong)
use "cooper_dec.ML"
use "cooper_proof.ML"