src/HOL/Library/RBT_Impl.thy
changeset 61585 a9599d3d7610
parent 61433 a4c0de1df3d8
child 62093 bd73a2279fcd
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Thu Nov 05 10:35:37 2015 +0100
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Thu Nov 05 10:39:49 2015 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  begin
     1.5  
     1.6  text \<open>
     1.7 -  For applications, you should use theory @{text RBT} which defines
     1.8 +  For applications, you should use theory \<open>RBT\<close> which defines
     1.9    an abstract type of red-black tree obeying the invariant.
    1.10  \<close>
    1.11  
    1.12 @@ -305,7 +305,7 @@
    1.13    "inv1 Empty = True"
    1.14  | "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)"
    1.15  
    1.16 -primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- \<open>Weaker version\<close>
    1.17 +primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close>
    1.18  where
    1.19    "inv1l Empty = True"
    1.20  | "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)"