register tree with datatype_compat ot support QuickCheck
authorhoelzl
Thu, 17 Jul 2014 14:55:56 +0200
changeset 57569 e20a999f7161
parent 57568 2c65870c706f
child 57570 70fcc6428393
register tree with datatype_compat ot support QuickCheck
src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Jul 17 10:29:09 2014 +0200
+++ b/src/HOL/Library/Tree.thy	Thu Jul 17 14:55:56 2014 +0200
@@ -10,6 +10,7 @@
   where
     "left Leaf = Leaf"
   | "right Leaf = Leaf"
+datatype_compat tree
 
 lemma neq_Leaf_iff: "(t \<noteq> Leaf) = (\<exists>l a r. t = Node l a r)"
   by (cases t) auto