# HG changeset patch # User krauss # Date 1161871720 -7200 # Node ID 51599a81b30804140029109aa820f8ed24e8ef52 # Parent 9e812f9f3a97c6868df6e7e36e6e6963f594c114 Added "recdef_wf" and "simp" attribute to "wf_measures" diff -r 9e812f9f3a97 -r 51599a81b308 src/HOL/List.thy --- a/src/HOL/List.thy Thu Oct 26 15:46:39 2006 +0200 +++ b/src/HOL/List.thy Thu Oct 26 16:08:40 2006 +0200 @@ -2411,7 +2411,7 @@ definition "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)" -lemma wf_measures: "wf (measures fs)" +lemma wf_measures[recdef_wf, simp]: "wf (measures fs)" unfolding measures_def by blast