equal
deleted
inserted
replaced
114 |
114 |
115 val split_rule_ss = HOL_basic_ss addsimps [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}]; |
115 val split_rule_ss = HOL_basic_ss addsimps [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}]; |
116 |
116 |
117 fun split_rule_goal ctxt xss rl = |
117 fun split_rule_goal ctxt xss rl = |
118 let |
118 let |
119 fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i); |
119 fun one_split i s = Tactic.rule_by_tactic ctxt (pair_tac ctxt s i); |
120 fun one_goal (i, xs) = fold (one_split (i + 1)) xs; |
120 fun one_goal (i, xs) = fold (one_split (i + 1)) xs; |
121 in |
121 in |
122 rl |
122 rl |
123 |> fold_index one_goal xss |
123 |> fold_index one_goal xss |
124 |> Simplifier.full_simplify split_rule_ss |
124 |> Simplifier.full_simplify split_rule_ss |