equal
deleted
inserted
replaced
80 (*We use a MINIMAL simpset because others (such as FOL_ss) contain too many |
80 (*We use a MINIMAL simpset because others (such as FOL_ss) contain too many |
81 simplifications. If the premises get simplified, then the proofs will |
81 simplifications. If the premises get simplified, then the proofs will |
82 fail. *) |
82 fail. *) |
83 val min_ss = empty_ss |
83 val min_ss = empty_ss |
84 setmksimps (map mk_meta_eq o ZF_atomize o gen_all) |
84 setmksimps (map mk_meta_eq o ZF_atomize o gen_all) |
85 setsolver (fn prems => resolve_tac (triv_rls@prems) |
85 setSolver (fn prems => resolve_tac (triv_rls@prems) |
86 ORELSE' assume_tac |
86 ORELSE' assume_tac |
87 ORELSE' etac FalseE); |
87 ORELSE' etac FalseE); |
88 |
88 |
89 val quant_induct = |
89 val quant_induct = |
90 prove_goalw_cterm part_rec_defs |
90 prove_goalw_cterm part_rec_defs |