src/HOL/WF_Rel.ML
changeset 9108 9fff97d29837
parent 9076 108ec332625d
child 9163 4d624e34e19a
     1.1 --- a/src/HOL/WF_Rel.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/WF_Rel.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4  val measure_induct = standard
     1.5      (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
     1.6        (wf_measure RS wf_induct));
     1.7 -store_thm("measure_induct",measure_induct);
     1.8 +bind_thm ("measure_induct", measure_induct);
     1.9  
    1.10  (*----------------------------------------------------------------------------
    1.11   * Wellfoundedness of lexicographic combinations