src/HOL/BNF/Examples/Misc_Datatype.thy
changeset 53134 4f8e156d2f19
parent 53123 00d922eba913
child 54193 bc07627c5dcd
--- a/src/HOL/BNF/Examples/Misc_Datatype.thy	Wed Aug 21 22:40:55 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Datatype.thy	Thu Aug 22 08:42:27 2013 +0200
@@ -56,6 +56,8 @@
 and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
 and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
 
+datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
+
 datatype_new ('a, 'b, 'c) some_killing =
   SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
 and ('a, 'b, 'c) in_here =