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