imp_conv_disj is now declared as a "code unfold" lemma to avoid that
authorberghofe
Tue Jan 08 10:24:34 2008 +0100 (2008-01-08)
changeset 25860844ab7ace3db
parent 25859 9bc18bf8be2d
child 25861 494d9301cc75
imp_conv_disj is now declared as a "code unfold" lemma to avoid that
conclusion is evaluated eagerly.
src/HOL/Code_Setup.thy
     1.1 --- a/src/HOL/Code_Setup.thy	Mon Jan 07 11:40:20 2008 +0100
     1.2 +++ b/src/HOL/Code_Setup.thy	Tue Jan 08 10:24:34 2008 +0100
     1.3 @@ -84,7 +84,7 @@
     1.4  
     1.5  text {* type bool *}
     1.6  
     1.7 -lemmas [code] = imp_conv_disj
     1.8 +lemmas [code unfold] = imp_conv_disj
     1.9  
    1.10  code_type bool
    1.11    (SML "bool")