| changeset 45969 | 562e99c3d316 |
| parent 45524 | 43ca06e6c168 |
| child 46320 | 0b8b73b49848 |
--- a/src/HOL/TPTP/CASC_Setup.thy Sat Dec 24 15:53:10 2011 +0100 +++ b/src/HOL/TPTP/CASC_Setup.thy Sat Dec 24 15:53:10 2011 +0100 @@ -89,8 +89,6 @@ lemma inj_of_rat [intro, simp]: "inj (of_rat\<Colon>rat\<Rightarrow>real)" by (metis injI of_rat_eq_iff rat_to_real_def) -declare mem_def [simp add] - declare [[smt_oracle]] refute_params [maxtime = 10000, no_assms, expect = genuine]