src/HOL/Library/RBT_Impl.thy
changeset 62093 bd73a2279fcd
parent 61585 a9599d3d7610
child 62390 842917225d56
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Thu Jan 07 15:50:09 2016 +0100
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Thu Jan 07 15:53:39 2016 +0100
     1.3 @@ -1758,9 +1758,7 @@
     1.4    Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse
     1.5    compare.simps compare.exhaust compare.induct compare.rec compare.simps
     1.6    compare.size compare.case_cong compare.case_cong_weak compare.case
     1.7 -  compare.nchotomy compare.split compare.split_asm rec_compare_def
     1.8 -  compare.eq.refl compare.eq.simps
     1.9 -  compare.EQ_def compare.GT_def compare.LT_def
    1.10 +  compare.nchotomy compare.split compare.split_asm compare.eq.refl compare.eq.simps
    1.11    equal_compare_def
    1.12    skip_red.simps skip_red.cases skip_red.induct 
    1.13    skip_black_def