src/HOL/Library/RBT_Impl.thy
changeset 61121 efe8b18306b7
parent 61076 bdc1e2f0a86a
child 61225 1a690dce8cfc
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Sun Sep 06 19:09:20 2015 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sun Sep 06 21:55:13 2015 +0200
     1.3 @@ -1757,9 +1757,9 @@
     1.4    compare.eq.refl compare.eq.simps
     1.5    compare.EQ_def compare.GT_def compare.LT_def
     1.6    equal_compare_def
     1.7 -  skip_red_def skip_red.simps skip_red.cases skip_red.induct 
     1.8 +  skip_red.simps skip_red.cases skip_red.induct 
     1.9    skip_black_def
    1.10 -  compare_height_def compare_height.simps
    1.11 +  compare_height.simps
    1.12  
    1.13  subsection \<open>union and intersection of sorted associative lists\<close>
    1.14