tuned
authorkrauss
Tue Jul 28 08:49:03 2009 +0200 (2009-07-28)
changeset 322450c1cb95a434d
parent 32244 a99723d77ae0
child 32246 d4f7934e9555
child 32263 8bc0fd4a23a0
tuned
src/HOL/Library/RBT.thy
     1.1 --- a/src/HOL/Library/RBT.thy	Tue Jul 28 08:48:56 2009 +0200
     1.2 +++ b/src/HOL/Library/RBT.thy	Tue Jul 28 08:49:03 2009 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  datatype color = R | B
     1.5  datatype ('a,'b)"rbt" = Empty | Tr color "('a,'b)rbt" 'a 'b "('a,'b)rbt"
     1.6  
     1.7 -(* Suchbaum-Eigenschaften *)
     1.8 +text {* Search tree properties *}
     1.9  
    1.10  primrec
    1.11    pin_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> bool"
    1.12 @@ -340,9 +340,6 @@
    1.13  
    1.14  subsection {* Deletion *}
    1.15  
    1.16 -(*definition
    1.17 -  [simp]: "ibn t = (bh t > 0 \<and> treec t = B)"
    1.18 -*)
    1.19  lemma bh_paintR'[simp]: "treec t = B \<Longrightarrow> bh (paint R t) = bh t - 1"
    1.20  by (cases t rule: rbt_cases) auto
    1.21