src/HOL/Data_Structures/AA_Set.thy
changeset 69505 cc2d676d5395
parent 68440 6826718f732d
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Wed Dec 26 16:07:28 2018 +0100
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Wed Dec 26 16:25:20 2018 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4  text\<open>In the paper, the last case of @{const adjust} is expressed with the help of an
     1.5  incorrect auxiliary function \texttt{nlvl}.
     1.6  
     1.7 -Function @{text split_max} below is called \texttt{dellrg} in the paper.
     1.8 +Function \<open>split_max\<close> below is called \texttt{dellrg} in the paper.
     1.9  The latter is incorrect for two reasons: \texttt{dellrg} is meant to delete the largest
    1.10  element but recurses on the left instead of the right subtree; the invariant
    1.11  is not restored.\<close>