author | oheimb |
Wed, 12 Nov 1997 12:23:37 +0100 | |
changeset 4203 | ca73de799b73 |
parent 4202 | 96876d71eef5 |
child 4204 | 7b15e7eee982 |
--- a/src/FOL/simpdata.ML Wed Nov 12 12:22:56 1997 +0100 +++ b/src/FOL/simpdata.ML Wed Nov 12 12:23:37 1997 +0100 @@ -183,8 +183,8 @@ fun split_inside_tac splits = mktac (map mk_meta_eq splits) end; -val split_prem_tac = mk_case_split_prem_tac split_tac disjE conjE exE contrapos - contrapos2 notnotD; +val split_asm_tac = mk_case_split_asm_tac split_tac + (disjE,conjE,exE,contrapos,contrapos2,notnotD); (*** Standard simpsets ***)