src/HOL/BNF/Examples/Misc_Data.thy
changeset 52813 963297a24206
parent 52323 a11bbb5fef56
child 52844 66fa0f602cc4
--- a/src/HOL/BNF/Examples/Misc_Data.thy	Wed Jul 31 15:24:07 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Data.thy	Wed Jul 31 16:50:41 2013 +0200
@@ -150,6 +150,8 @@
 and s8 = S8 nat
 *)
 
+datatype_new 'a deadbar = DeadBar "'a \<Rightarrow> 'a"
+datatype_new 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
 datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
 datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"