equal
deleted
inserted
replaced
1755 compare.size compare.case_cong compare.case_cong_weak compare.case |
1755 compare.size compare.case_cong compare.case_cong_weak compare.case |
1756 compare.nchotomy compare.split compare.split_asm rec_compare_def |
1756 compare.nchotomy compare.split compare.split_asm rec_compare_def |
1757 compare.eq.refl compare.eq.simps |
1757 compare.eq.refl compare.eq.simps |
1758 compare.EQ_def compare.GT_def compare.LT_def |
1758 compare.EQ_def compare.GT_def compare.LT_def |
1759 equal_compare_def |
1759 equal_compare_def |
1760 skip_red_def skip_red.simps skip_red.cases skip_red.induct |
1760 skip_red.simps skip_red.cases skip_red.induct |
1761 skip_black_def |
1761 skip_black_def |
1762 compare_height_def compare_height.simps |
1762 compare_height.simps |
1763 |
1763 |
1764 subsection \<open>union and intersection of sorted associative lists\<close> |
1764 subsection \<open>union and intersection of sorted associative lists\<close> |
1765 |
1765 |
1766 context ord begin |
1766 context ord begin |
1767 |
1767 |