equal
deleted
inserted
replaced
29 - Added predicates irrefl_on and irreflp_on and redefined irrefl and |
29 - Added predicates irrefl_on and irreflp_on and redefined irrefl and |
30 irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are |
30 irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are |
31 explicitly provided for backward compatibility but their usage is |
31 explicitly provided for backward compatibility but their usage is |
32 discouraged. Minor INCOMPATIBILITY. |
32 discouraged. Minor INCOMPATIBILITY. |
33 - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY. |
33 - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY. |
|
34 preorder.irreflp_greater[simp] ~> irreflp_on_greater[simp] |
|
35 preorder.irreflp_less[simp] ~> irreflp_on_less[simp] |
|
36 reflp_equality[simp] ~> reflp_on_equality[simp] |
34 total_on_singleton |
37 total_on_singleton |
35 reflp_equality[simp] ~> reflp_on_equality[simp] |
|
36 - Added lemmas. |
38 - Added lemmas. |
37 antisym_if_asymp |
39 antisym_if_asymp |
38 antisymp_if_asymp |
40 antisymp_if_asymp |
39 irrefl_onD |
41 irrefl_onD |
40 irrefl_onI |
42 irrefl_onI |