equal
deleted
inserted
replaced
122 |> RuleCases.save rl |
122 |> RuleCases.save rl |
123 end; |
123 end; |
124 |
124 |
125 |
125 |
126 fun pair_tac ctxt s = |
126 fun pair_tac ctxt s = |
127 RuleInsts.res_inst_tac ctxt [(("p", 0), s)] @{thm PairE} |
127 res_inst_tac ctxt [(("p", 0), s)] @{thm PairE} |
128 THEN' hyp_subst_tac |
128 THEN' hyp_subst_tac |
129 THEN' K prune_params_tac; |
129 THEN' K prune_params_tac; |
130 |
130 |
131 val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv]; |
131 val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv]; |
132 |
132 |