equal
deleted
inserted
replaced
123 |> Drule.implies_intr_list subgoals |
123 |> Drule.implies_intr_list subgoals |
124 |> fold_rev (Thm.forall_intr o #1) subgoal_inst |
124 |> fold_rev (Thm.forall_intr o #1) subgoal_inst |
125 |> fold (Thm.forall_elim o #2) subgoal_inst |
125 |> fold (Thm.forall_elim o #2) subgoal_inst |
126 |> Thm.adjust_maxidx_thm idx |
126 |> Thm.adjust_maxidx_thm idx |
127 |> singleton (Variable.export ctxt2 ctxt0); |
127 |> singleton (Variable.export ctxt2 ctxt0); |
128 in Thm.bicompose false (false, result, Thm.nprems_of st1) i st0 end; |
128 in |
|
129 Thm.bicompose {flatten = true, match = false, incremented = false} |
|
130 (false, result, Thm.nprems_of st1) i st0 |
|
131 end; |
129 |
132 |
130 |
133 |
131 (* tacticals *) |
134 (* tacticals *) |
132 |
135 |
133 fun GEN_FOCUS flags tac ctxt i st = |
136 fun GEN_FOCUS flags tac ctxt i st = |