| changeset 371 | 3a853818f1d2 |
| parent 282 | 731b27c90d2f |
| child 394 | 432bb9995893 |
--- 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];