Lines Matching refs:final
71 Need both initial goal and final theorem in PROVED case, because
81 final : thm -> thm,
106 then GSTK{prop=POSED g, stack=[], final=f}
109 fun finalizer(GSTK{final,...}) = final;
116 | rotate(GSTK{prop, stack, final}) n =
125 else GSTK{prop=prop, final=final,
133 fun return(GSTK{stack={goals=[],validation}::rst, prop as POSED g,final}) =
137 (let val thm = final th
138 in GSTK{prop=PROVED (thm,g), stack=[], final=final}
145 return(GSTK{prop=prop, final=final,
154 | expand_msg dpth (GSTK{prop, final, stack as {goals, ...}::_}) =
170 | expandf tac (GSTK{prop as POSED g, stack,final}) =
174 val gs = return(GSTK{prop=prop,final=final,
181 | expand_listf ltac (GSTK{prop as POSED g, stack = [], final}) =
183 stack = [{goals = [g], validation = hd}], final = final})
184 | expand_listf ltac (GSTK{prop, stack as {goals,validation}::rst, final}) =
187 val new_gs = return (GSTK{prop=prop, final=final,
201 final} =>
210 GSTK {prop = prop, stack = newgv :: rst, final = final}
217 | flatn (gstk as GSTK{prop, stack = [], final}) n = gstk
218 | flatn (gstk as GSTK{prop, stack as [_], final}) n = gstk
219 | flatn (gstk as GSTK{prop, stack, final}) n = flatn (flat gstk) (n-1) ;