equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/TFL/post.ML |
1 (* Title: HOL/Tools/TFL/post.ML |
2 ID: $Id$ |
|
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
2 Author: Konrad Slind, Cambridge University Computer Laboratory |
4 Copyright 1997 University of Cambridge |
3 Copyright 1997 University of Cambridge |
5 |
4 |
6 Second part of main module (postprocessing of TFL definitions). |
5 Second part of main module (postprocessing of TFL definitions). |
7 *) |
6 *) |
29 * Extract termination goals so that they can be put it into a goalstack, or |
28 * Extract termination goals so that they can be put it into a goalstack, or |
30 * have a tactic directly applied to them. |
29 * have a tactic directly applied to them. |
31 *--------------------------------------------------------------------------*) |
30 *--------------------------------------------------------------------------*) |
32 fun termination_goals rules = |
31 fun termination_goals rules = |
33 map (Type.freeze o HOLogic.dest_Trueprop) |
32 map (Type.freeze o HOLogic.dest_Trueprop) |
34 (foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules); |
33 (List.foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules); |
35 |
34 |
36 (*--------------------------------------------------------------------------- |
35 (*--------------------------------------------------------------------------- |
37 * Finds the termination conditions in (highly massaged) definition and |
36 * Finds the termination conditions in (highly massaged) definition and |
38 * puts them into a goalstack. |
37 * puts them into a goalstack. |
39 *--------------------------------------------------------------------------*) |
38 *--------------------------------------------------------------------------*) |