src/HOL/Datatype.thy
changeset 17458 e42bfad176eb
parent 15140 322485b816ac
child 17876 b9c92f384109
--- 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