tuned
authorhaftmann
Thu Mar 20 12:01:14 2008 +0100 (2008-03-20)
changeset 263527f50b708376c
parent 26351 d5125a62f839
child 26353 537ff6997149
tuned
src/HOL/Tools/split_rule.ML
     1.1 --- a/src/HOL/Tools/split_rule.ML	Thu Mar 20 12:01:13 2008 +0100
     1.2 +++ b/src/HOL/Tools/split_rule.ML	Thu Mar 20 12:01:14 2008 +0100
     1.3 @@ -123,6 +123,9 @@
     1.4    end;
     1.5  
     1.6  
     1.7 +fun pair_tac s =
     1.8 +  EVERY' [res_inst_tac [("p", s)] @{thm PairE}, hyp_subst_tac, K prune_params_tac];
     1.9 +
    1.10  val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
    1.11  
    1.12  fun split_rule_goal xss rl =