src/HOL/BNF/Examples/Misc_Datatype.thy
changeset 53123 00d922eba913
parent 53122 bc87b7af4767
child 53134 4f8e156d2f19
equal deleted inserted replaced
53122:bc87b7af4767 53123:00d922eba913
   152 
   152 
   153 datatype_new 'a deadbar = DeadBar "'a \<Rightarrow> 'a"
   153 datatype_new 'a deadbar = DeadBar "'a \<Rightarrow> 'a"
   154 datatype_new 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
   154 datatype_new 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
   155 datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
   155 datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
   156 datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
   156 datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
   157 datatype_new 'a deadfoo = C "'a \<Rightarrow> 'a + 'a"
   157 datatype_new 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a"
   158 
   158 
   159 datatype_new 'a dead_foo = A
   159 datatype_new 'a dead_foo = A
   160 datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
   160 datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
   161 
   161 
   162 datatype_new d1 = D
   162 datatype_new d1 = D