# HG changeset patch
# User nipkow
# Date 1434571616 -7200
# Node ID 16993a3f4967e35914855d7f51df0e2e1a5fb0db
# Parent  83231b558ce429c283bffb72aa39c2c1d5ca28e2
tuned

diff -r 83231b558ce4 -r 16993a3f4967 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Wed Jun 17 20:22:01 2015 +0200
+++ b/src/HOL/Library/Tree.thy	Wed Jun 17 22:06:56 2015 +0200
@@ -24,7 +24,7 @@
   "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
 by (simp_all add: size1_def)
 
-lemma size_0_iff_Leaf[simp]: "size t = 0 \<longleftrightarrow> t = Leaf"
+lemma size_0_iff_Leaf: "size t = 0 \<longleftrightarrow> t = Leaf"
 by(cases t) auto
 
 lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)"