# HG changeset patch
# User haftmann
# Date 1200410359 -3600
# Node ID d957d9982241d526f51cfabc0d9ebd013b45c21b
# Parent  f1bce5261decb78b08cf0784f82d270a26b12b23
explicit code lemma for implication

diff -r f1bce5261dec -r d957d9982241 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")