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