src/HOL/Library/RBT_Impl.thy
changeset 57983 6edc3529bb4e
parent 57512 cc97b347b301
child 58249 180f1b3508ed
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -1754,7 +1754,7 @@
     1.4    Abs_compare_cases Abs_compare_induct Abs_compare_inject Abs_compare_inverse
     1.5    Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse
     1.6    compare.simps compare.exhaust compare.induct compare.rec compare.simps
     1.7 -  compare.size compare.case_cong compare.weak_case_cong compare.case
     1.8 +  compare.size compare.case_cong compare.case_cong_weak compare.case
     1.9    compare.nchotomy compare.split compare.split_asm rec_compare_def
    1.10    compare.eq.refl compare.eq.simps
    1.11    compare.EQ_def compare.GT_def compare.LT_def