Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Tree.thy
changeset 57569 e20a999f7161
parent 57530 439f881c8744
child 57687 cca7e8788481 
--- 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
isabelle