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