| changeset 26749 | 397a1aeede7d |
| parent 26748 | 4d51ddd6aa5c |
| child 26989 | 9b2acb536228 |
--- a/src/HOL/Tools/function_package/fundef_common.ML Fri Apr 25 15:30:33 2008 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Fri Apr 25 16:28:06 2008 +0200 @@ -119,6 +119,11 @@ val all_fundef_data = NetRules.rules o FundefData.get +structure TerminationSimps = NamedThmsFun( + val name = "termination_simp" + val description = "Simplification rule for termination proofs" +); + structure TerminationRule = GenericDataFun ( type T = thm list