lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
authorwenzelm
Sat Sep 17 18:11:18 2005 +0200 (2005-09-17)
changeset 17458e42bfad176eb
parent 17457 5b9538fc6d67
child 17459 9a3925c07392
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
src/HOL/Datatype.thy
     1.1 --- a/src/HOL/Datatype.thy	Sat Sep 17 18:11:17 2005 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Sat Sep 17 18:11:18 2005 +0200
     1.3 @@ -206,4 +206,6 @@
     1.4    apply (simp split add: sum.split)
     1.5    done
     1.6  
     1.7 +lemmas [code] = imp_conv_disj
     1.8 +
     1.9  end