renamed split_prem_tac to split_asm_tac
authoroheimb
Wed, 12 Nov 1997 12:23:37 +0100
changeset 4203 ca73de799b73
parent 4202 96876d71eef5
child 4204 7b15e7eee982
renamed split_prem_tac to split_asm_tac
src/FOL/simpdata.ML
--- 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 ***)