--- a/src/HOL/WF_Rel.ML Fri Feb 20 17:57:16 1998 +0100
+++ b/src/HOL/WF_Rel.ML Sun Feb 22 14:12:23 1998 +0100
@@ -59,6 +59,11 @@
qed "wf_measure";
AddIffs [wf_measure];
+val measure_induct = standard
+ (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
+ (wf_measure RS wf_induct));
+store_thm("measure_induct",measure_induct);
+
(*----------------------------------------------------------------------------
* Wellfoundedness of lexicographic combinations
*---------------------------------------------------------------------------*)