# HG changeset patch
# User nipkow
# Date 1505675042 -7200
# Node ID d5bf4bdb4fb7231368e589e631dbc36c14fcee00
# Parent  59acf5e73176393fcd34d900e3bd4a85f3597bde
added lemmas

diff -r 59acf5e73176 -r d5bf4bdb4fb7 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Sep 14 19:21:32 2017 +0200
+++ b/src/HOL/Library/Tree.thy	Sun Sep 17 21:04:02 2017 +0200
@@ -475,6 +475,12 @@
 lemma height_mirror[simp]: "height(mirror t) = height t"
 by (induction t) simp_all
 
+lemma min_height_mirror [simp]: "min_height (mirror t) = min_height t"
+by (induction t) simp_all  
+
+lemma ipl_mirror [simp]: "ipl (mirror t) = ipl t"
+by (induction t) simp_all
+
 lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)"
 by (induction t) simp_all