# HG changeset patch # User lcp # Date 768821155 -7200 # Node ID 3a853818f1d224c1ea4da956fef8c865826e6ee3 # Parent e95e212512d18ed8f73222eda6c945e1cfea7d24 FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the simplifier can rewrite premises, it can generate the premise False." diff -r e95e212512d1 -r 3a853818f1d2 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Fri May 13 11:10:14 1994 +0200 +++ b/src/FOL/simpdata.ML Fri May 13 11:25:55 1994 +0200 @@ -95,7 +95,9 @@ val IFOL_ss = empty_ss setmksimps (map mk_meta_eq o atomize o gen_all) - setsolver (fn prems => resolve_tac (triv_rls@prems) ORELSE' assume_tac) + setsolver (fn prems => resolve_tac (triv_rls@prems) + ORELSE' assume_tac + ORELSE' etac FalseE) setsubgoaler asm_simp_tac addsimps IFOL_rews addcongs [imp_cong];