equal
deleted
inserted
replaced
148 map_filter (fn (t, u) => |
148 map_filter (fn (t, u) => |
149 (case abstr (getP u) of |
149 (case abstr (getP u) of |
150 NONE => NONE |
150 NONE => NONE |
151 | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u'))) (ts ~~ ts'); |
151 | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u'))) (ts ~~ ts'); |
152 val indrule' = cterm_instantiate insts indrule; |
152 val indrule' = cterm_instantiate insts indrule; |
153 in resolve_tac [indrule'] i end); |
153 in resolve0_tac [indrule'] i end); |
154 |
154 |
155 |
155 |
156 (* perform exhaustive case analysis on last parameter of subgoal i *) |
156 (* perform exhaustive case analysis on last parameter of subgoal i *) |
157 |
157 |
158 fun exh_tac ctxt exh_thm_of = CSUBGOAL (fn (cgoal, i) => |
158 fun exh_tac ctxt exh_thm_of = CSUBGOAL (fn (cgoal, i) => |