author | paulson |
Tue, 04 Aug 2020 11:45:03 +0100 | |
changeset 72092 | 3f8e6c0166ac |
parent 72080 | 2030eacf3a72 (diff) |
parent 72091 | b6065cbbf5e2 (current diff) |
child 72093 | 6a2f43901350 |
--- a/src/HOL/Data_Structures/Tree2.thy Mon Aug 03 11:46:19 2020 +0100 +++ b/src/HOL/Data_Structures/Tree2.thy Tue Aug 04 11:45:03 2020 +0100 @@ -36,4 +36,7 @@ lemma set_inorder[simp]: "set (inorder t) = set_tree t" by (induction t) auto +lemma length_inorder[simp]: "length (inorder t) = size t" +by (induction t) auto + end