# HG changeset patch
# User bulwahn
# Date 1327928119 -3600
# Node ID 48fcca8965f4e4aad164a5facc7ca2c15e96838d
# Parent  42a01315d9986d43c272251f771b7db0db9be926
adding code_unfold to make measure executable

diff -r 42a01315d998 -r 48fcca8965f4 src/HOL/Wellfounded.thy
--- 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)"