equal
deleted
inserted
replaced
981 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" |
981 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" |
982 by (simp cong: conj_cong) |
982 by (simp cong: conj_cong) |
983 |
983 |
984 use "cooper_dec.ML" |
984 use "cooper_dec.ML" |
985 oracle |
985 oracle |
986 presburger_oracle = CooperDec.mk_presburger_oracle |
986 presburger_oracle ("term") = CooperDec.presburger_oracle |
987 |
987 |
988 use "cooper_proof.ML" |
988 use "cooper_proof.ML" |
989 use "qelim.ML" |
989 use "qelim.ML" |
990 use "presburger.ML" |
990 use "presburger.ML" |
991 |
991 |