| changeset 26352 | 7f50b708376c |
| parent 25979 | 3297781f8141 |
| child 27208 | 5fe899199f85 |
--- a/src/HOL/Tools/split_rule.ML Thu Mar 20 12:01:13 2008 +0100 +++ b/src/HOL/Tools/split_rule.ML Thu Mar 20 12:01:14 2008 +0100 @@ -123,6 +123,9 @@ end; +fun pair_tac s = + EVERY' [res_inst_tac [("p", s)] @{thm PairE}, hyp_subst_tac, K prune_params_tac]; + val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv]; fun split_rule_goal xss rl =