src/HOL/Library/RBT_Impl.thy
changeset 63680 6e1e8b5abbfa
parent 63649 e690d6f2185b
child 64243 aee949f6642d
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Aug 12 17:49:02 2016 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Aug 12 17:53:55 2016 +0200
     1.3 @@ -551,8 +551,10 @@
     1.4  lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
     1.5  by (cases t rule: rbt_cases) auto
     1.6  
     1.7 -text \<open>The function definitions are based on the Haskell code by Stefan Kahrs
     1.8 -at @{url "http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html"} .\<close>
     1.9 +text \<open>
    1.10 +  The function definitions are based on the Haskell code by Stefan Kahrs
    1.11 +  at \<^url>\<open>http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html\<close>.
    1.12 +\<close>
    1.13  
    1.14  fun
    1.15    balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"