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