changeset 46356 | 48fcca8965f4 |
parent 46349 | b159ca4e268b |
child 46635 | cde737f9c911 |
--- a/src/HOL/Wellfounded.thy Sun Jan 29 15:16:27 2012 +0100 +++ b/src/HOL/Wellfounded.thy Mon Jan 30 13:55:19 2012 +0100 @@ -635,7 +635,7 @@ definition measure :: "('a => nat) => ('a * 'a)set" where "measure = inv_image less_than" -lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)" +lemma in_measure[simp, code_unfold]: "((x,y) : measure f) = (f x < f y)" by (simp add:measure_def) lemma wf_measure [iff]: "wf (measure f)"