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"