src/HOL/Data_Structures/AA_Set.thy
changeset 67406 23307fd33906
parent 67369 7360fe6bb423
child 67613 ce654b0e6d69
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Thu Jan 11 13:48:17 2018 +0100
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Fri Jan 12 14:08:53 2018 +0100
     1.3 @@ -69,13 +69,13 @@
     1.4                 \<Rightarrow> Node (lva+1) (Node (lv-1) l x t2) a
     1.5                      (split (Node (if sngl t1 then lva else lva+1) t3 b t4)))))"
     1.6  
     1.7 -text{* In the paper, the last case of @{const adjust} is expressed with the help of an
     1.8 +text\<open>In the paper, the last case of @{const adjust} is expressed with the help of an
     1.9  incorrect auxiliary function \texttt{nlvl}.
    1.10  
    1.11  Function @{text del_max} below is called \texttt{dellrg} in the paper.
    1.12  The latter is incorrect for two reasons: \texttt{dellrg} is meant to delete the largest
    1.13  element but recurses on the left instead of the right subtree; the invariant
    1.14 -is not restored.*}
    1.15 +is not restored.\<close>
    1.16  
    1.17  fun del_max :: "'a aa_tree \<Rightarrow> 'a aa_tree * 'a" where
    1.18  "del_max (Node lv l a Leaf) = (l,a)" |
    1.19 @@ -269,7 +269,7 @@
    1.20            by (auto simp add: skew_invar split_invar)
    1.21        next
    1.22          case (Incr)
    1.23 -        thus ?thesis using invar_NodeR2[OF `invar ?t` Incr(2) 1 iir] 1 \<open>x < a\<close>
    1.24 +        thus ?thesis using invar_NodeR2[OF \<open>invar ?t\<close> Incr(2) 1 iir] 1 \<open>x < a\<close>
    1.25            by (auto simp add: skew_invar split_invar split: if_splits)
    1.26        qed
    1.27      qed