# HG changeset patch
# User wenzelm
# Date 1126973478 -7200
# Node ID e42bfad176eb50072a5101429e707795c8c8dac5
# Parent  5b9538fc6d679982b605fcc78e2d1985cd4acced
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?

diff -r 5b9538fc6d67 -r e42bfad176eb src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Sat Sep 17 18:11:17 2005 +0200
+++ b/src/HOL/Datatype.thy	Sat Sep 17 18:11:18 2005 +0200
@@ -206,4 +206,6 @@
   apply (simp split add: sum.split)
   done
 
+lemmas [code] = imp_conv_disj
+
 end