# HG changeset patch
# User krauss
# Date 1248763743 -7200
# Node ID 0c1cb95a434d8f1ca0dec5370d5cf3bf2f37b2f8
# Parent  a99723d77ae049aa7f4feccc5d0ccab7e89dd57f
tuned

diff -r a99723d77ae0 -r 0c1cb95a434d src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Tue Jul 28 08:48:56 2009 +0200
+++ b/src/HOL/Library/RBT.thy	Tue Jul 28 08:49:03 2009 +0200
@@ -13,7 +13,7 @@
 datatype color = R | B
 datatype ('a,'b)"rbt" = Empty | Tr color "('a,'b)rbt" 'a 'b "('a,'b)rbt"
 
-(* Suchbaum-Eigenschaften *)
+text {* Search tree properties *}
 
 primrec
   pin_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> bool"
@@ -340,9 +340,6 @@
 
 subsection {* Deletion *}
 
-(*definition
-  [simp]: "ibn t = (bh t > 0 \<and> treec t = B)"
-*)
 lemma bh_paintR'[simp]: "treec t = B \<Longrightarrow> bh (paint R t) = bh t - 1"
 by (cases t rule: rbt_cases) auto