# 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