author | hoelzl |
Thu, 17 Jul 2014 14:55:56 +0200 | |
changeset 57569 | e20a999f7161 |
parent 57568 | 2c65870c706f |
child 57570 | 70fcc6428393 |
--- 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