equal
deleted
inserted
replaced
75 functor Order_Tac_Fun (Less: LESS_ARITH): ORDER_TAC = |
75 functor Order_Tac_Fun (Less: LESS_ARITH): ORDER_TAC = |
76 struct |
76 struct |
77 |
77 |
78 (* Extract subgoal with signature *) |
78 (* Extract subgoal with signature *) |
79 fun SUBGOAL goalfun i st = |
79 fun SUBGOAL goalfun i st = |
80 goalfun (List.nth(prems_of st, i-1), i, sign_of_thm st) st |
80 goalfun (List.nth(prems_of st, i-1), i, Thm.theory_of_thm st) st |
81 handle Subscript => Seq.empty; |
81 handle Subscript => Seq.empty; |
82 |
82 |
83 (* Internal datatype for the proof *) |
83 (* Internal datatype for the proof *) |
84 datatype proof |
84 datatype proof |
85 = Asm of int |
85 = Asm of int |