equal
deleted
inserted
replaced
50 A ==> ... ==> #C |
50 A ==> ... ==> #C |
51 ---------------- (conclude) |
51 ---------------- (conclude) |
52 A ==> ... ==> C |
52 A ==> ... ==> C |
53 *) |
53 *) |
54 fun conclude th = |
54 fun conclude th = |
55 (case SINGLE (Thm.bicompose false (false, th, Thm.nprems_of th) 1) |
55 (case SINGLE (Thm.bicompose_no_flatten false (false, th, Thm.nprems_of th) 1) |
56 (Drule.incr_indexes th Drule.protectD) of |
56 (Drule.incr_indexes th Drule.protectD) of |
57 SOME th' => th' |
57 SOME th' => th' |
58 | NONE => raise THM ("Failed to conclude goal", 0, [th])); |
58 | NONE => raise THM ("Failed to conclude goal", 0, [th])); |
59 |
59 |
60 (* |
60 (* |
177 local |
177 local |
178 |
178 |
179 fun SELECT tac i st = |
179 fun SELECT tac i st = |
180 init (Thm.adjust_maxidx (Thm.cprem_of st i)) |
180 init (Thm.adjust_maxidx (Thm.cprem_of st i)) |
181 |> tac |
181 |> tac |
182 |> Seq.maps (fn st' => Thm.bicompose false (false, conclude st', Thm.nprems_of st') i st); |
182 |> Seq.maps (fn st' => |
|
183 Thm.bicompose_no_flatten false (false, conclude st', Thm.nprems_of st') i st); |
183 |
184 |
184 in |
185 in |
185 |
186 |
186 fun SELECT_GOAL tac i st = |
187 fun SELECT_GOAL tac i st = |
187 let val n = Thm.nprems_of st in |
188 let val n = Thm.nprems_of st in |