Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added "recdef_wf" and "simp" attribute to "wf_measures"
authorkrauss
Thu, 26 Oct 2006 16:08:40 +0200
changeset 21106 51599a81b308
parent 21105 9e812f9f3a97
child 21107 e69c0e82955a
Added "recdef_wf" and "simp" attribute to "wf_measures"
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle