explicit code lemma for implication
authorhaftmann
Tue Jan 15 16:19:19 2008 +0100 (2008-01-15)
changeset 25916d957d9982241
parent 25915 f1bce5261dec
child 25917 d6c920623afc
explicit code lemma for implication
src/HOL/Code_Setup.thy
     1.1 --- a/src/HOL/Code_Setup.thy	Tue Jan 15 02:38:13 2008 +0100
     1.2 +++ b/src/HOL/Code_Setup.thy	Tue Jan 15 16:19:19 2008 +0100
     1.3 @@ -86,7 +86,7 @@
     1.4  
     1.5  text {* type bool *}
     1.6  
     1.7 -lemmas [code unfold] = imp_conv_disj
     1.8 +lemmas [code func, code unfold] = imp_conv_disj
     1.9  
    1.10  code_type bool
    1.11    (SML "bool")