# HG changeset patch
# User berghofe
# Date 1199784274 -3600
# Node ID 844ab7ace3db3b61a2b36f5100374ad4df56e27f
# Parent  9bc18bf8be2d83dbb523b7e7192b9fcdb1403f72
imp_conv_disj is now declared as a "code unfold" lemma to avoid that
conclusion is evaluated eagerly.

diff -r 9bc18bf8be2d -r 844ab7ace3db src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Mon Jan 07 11:40:20 2008 +0100
+++ b/src/HOL/Code_Setup.thy	Tue Jan 08 10:24:34 2008 +0100
@@ -84,7 +84,7 @@
 
 text {* type bool *}
 
-lemmas [code] = imp_conv_disj
+lemmas [code unfold] = imp_conv_disj
 
 code_type bool
   (SML "bool")