| changeset 45231 | d85a2fdc586c | 
| parent 44928 | 7ef6505bde7f | 
| child 45461 | 130c90bb80b4 | 
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Fri Oct 21 11:17:14 2011 +0200 @@ -84,7 +84,7 @@ definition subtract where - [code_inline]: "subtract x y = y - x" + [code_unfold]: "subtract x y = y - x" setup {* let