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] |
34 preorder.irreflp_greater[simp] ~> preorder.irreflp_on_greater[simp] |
35 preorder.irreflp_less[simp] ~> irreflp_on_less[simp] |
35 preorder.irreflp_less[simp] ~> preorder.irreflp_on_less[simp] |
36 reflp_equality[simp] ~> reflp_on_equality[simp] |
36 reflp_equality[simp] ~> reflp_on_equality[simp] |
37 total_on_singleton |
37 total_on_singleton |
38 - Added lemmas. |
38 - Added lemmas. |
39 antisym_if_asymp |
39 antisym_if_asymp |
40 antisymp_if_asymp |
40 antisymp_if_asymp |
41 asym_if_irrefl_and_trans |
41 asym_if_irrefl_and_trans |
42 asymp_if_irreflp_and_transp |
42 asymp_if_irreflp_and_transp |
|
43 irreflD |
43 irrefl_onD |
44 irrefl_onD |
44 irrefl_onI |
45 irrefl_onI |
45 irrefl_on_converse[simp] |
46 irrefl_on_converse[simp] |
46 irrefl_on_subset |
47 irrefl_on_subset |
|
48 irreflpD |
47 irreflp_onD |
49 irreflp_onD |
48 irreflp_onI |
50 irreflp_onI |
49 irreflp_on_converse[simp] |
51 irreflp_on_converse[simp] |
50 irreflp_on_irrefl_on_eq[pred_set_conv] |
52 irreflp_on_irrefl_on_eq[pred_set_conv] |
51 irreflp_on_subset |
53 irreflp_on_subset |