equal
deleted
inserted
replaced
51 (*--------------------------------------------------------------------------- |
51 (*--------------------------------------------------------------------------- |
52 * Finds the termination conditions in (highly massaged) definition and |
52 * Finds the termination conditions in (highly massaged) definition and |
53 * puts them into a goalstack. |
53 * puts them into a goalstack. |
54 *--------------------------------------------------------------------------*) |
54 *--------------------------------------------------------------------------*) |
55 fun tgoalw thy defs rules = |
55 fun tgoalw thy defs rules = |
56 let val L = termination_goals rules |
56 case termination_goals rules of |
57 open USyntax |
57 [] => error "tgoalw: no termination conditions to prove" |
58 val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L)) |
58 | L => goalw_cterm defs |
59 in goalw_cterm defs g |
59 (cterm_of (sign_of thy) |
60 end; |
60 (HOLogic.mk_Trueprop(USyntax.list_mk_conj L))); |
61 |
61 |
62 fun tgoal thy = tgoalw thy []; |
62 fun tgoal thy = tgoalw thy []; |
63 |
63 |
64 (*--------------------------------------------------------------------------- |
64 (*--------------------------------------------------------------------------- |
65 * Three postprocessors are applied to the definition. It |
65 * Three postprocessors are applied to the definition. It |