equal
deleted
inserted
replaced
26 * Extract termination goals so that they can be put it into a goalstack, or |
26 * Extract termination goals so that they can be put it into a goalstack, or |
27 * have a tactic directly applied to them. |
27 * have a tactic directly applied to them. |
28 *--------------------------------------------------------------------------*) |
28 *--------------------------------------------------------------------------*) |
29 fun termination_goals rules = |
29 fun termination_goals rules = |
30 map (Type.freeze o HOLogic.dest_Trueprop) |
30 map (Type.freeze o HOLogic.dest_Trueprop) |
31 (List.foldr (fn (th,A) => uncurry (union (op aconv)) (prems_of th, A)) [] rules); |
31 (fold_rev (union (op aconv) o prems_of) rules []); |
32 |
32 |
33 (*--------------------------------------------------------------------------- |
33 (*--------------------------------------------------------------------------- |
34 * Three postprocessors are applied to the definition. It |
34 * Three postprocessors are applied to the definition. It |
35 * attempts to prove wellfoundedness of the given relation, simplifies the |
35 * attempts to prove wellfoundedness of the given relation, simplifies the |
36 * non-proved termination conditions, and finally attempts to prove the |
36 * non-proved termination conditions, and finally attempts to prove the |