src/HOL/Library/RBT_Impl.thy
changeset 55642 63beb38e9258
parent 55466 786edc984c98
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Feb 21 00:09:55 2014 +0100
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Feb 21 00:09:56 2014 +0100
     1.3 @@ -1753,8 +1753,8 @@
     1.4  hide_fact (open)
     1.5    Abs_compare_cases Abs_compare_induct Abs_compare_inject Abs_compare_inverse
     1.6    Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse
     1.7 -  compare.simps compare.exhaust compare.induct compare.recs compare.simps
     1.8 -  compare.size compare.case_cong compare.weak_case_cong compare.cases 
     1.9 +  compare.simps compare.exhaust compare.induct compare.rec compare.simps
    1.10 +  compare.size compare.case_cong compare.weak_case_cong compare.case
    1.11    compare.nchotomy compare.split compare.split_asm rec_compare_def
    1.12    compare.eq.refl compare.eq.simps
    1.13    compare.EQ_def compare.GT_def compare.LT_def