adding code_unfold to make measure executable
authorbulwahn
Mon Jan 30 13:55:19 2012 +0100 (2012-01-30)
changeset 4635648fcca8965f4
parent 46355 42a01315d998
child 46357 2795607a1f40
adding code_unfold to make measure executable
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Wellfounded.thy	Sun Jan 29 15:16:27 2012 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Mon Jan 30 13:55:19 2012 +0100
     1.3 @@ -635,7 +635,7 @@
     1.4  definition measure :: "('a => nat) => ('a * 'a)set"
     1.5  where "measure = inv_image less_than"
     1.6  
     1.7 -lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
     1.8 +lemma in_measure[simp, code_unfold]: "((x,y) : measure f) = (f x < f y)"
     1.9    by (simp add:measure_def)
    1.10  
    1.11  lemma wf_measure [iff]: "wf (measure f)"