# HG changeset patch
# User blanchet
# Date 1377153747 -7200
# Node ID 4f8e156d2f1917597046f4b8d8b78acfc8543d50
# Parent  427724cff97082d7912b0483e06f13181658d92a
added datatype example

diff -r 427724cff970 -r 4f8e156d2f19 src/HOL/BNF/Examples/Misc_Datatype.thy
--- 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 =