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"