src/HOL/Integ/Presburger.thy
 changeset 14758 af3b71a46a1c parent 14738 83f1a514dcb4 child 14941 1edb674e0c33
```     1.1 --- a/src/HOL/Integ/Presburger.thy	Wed May 19 11:21:19 2004 +0200
1.2 +++ b/src/HOL/Integ/Presburger.thy	Wed May 19 11:23:59 2004 +0200
1.3 @@ -978,11 +978,11 @@
1.4    \medskip Specific instances of congruence rules, to prevent
1.5    simplifier from looping. *}
1.6
1.7 -theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
1.8 +theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
1.9    by simp
1.10
1.11 -theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<and> P) = (0 <= x \<and> P')"
1.12 -  by simp
1.13 +theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
1.14 +  by (simp cong: conj_cong)
1.15
1.16  use "cooper_dec.ML"
1.17  use "cooper_proof.ML"
```