equal
deleted
inserted
replaced
43 order.antisymp_le[simp] |
43 order.antisymp_le[simp] |
44 preorder.antisymp_greater[simp] |
44 preorder.antisymp_greater[simp] |
45 preorder.antisymp_less[simp] |
45 preorder.antisymp_less[simp] |
46 preorder.reflp_ge[simp] |
46 preorder.reflp_ge[simp] |
47 preorder.reflp_le[simp] |
47 preorder.reflp_le[simp] |
|
48 reflp_on_conversp[simp] |
48 totalp_on_singleton[simp] |
49 totalp_on_singleton[simp] |
49 |
50 |
50 * Theory "HOL.Transitive_Closure": |
51 * Theory "HOL.Transitive_Closure": |
51 - Strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp. |
52 - Strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp. |
52 Minor INCOMPATIBILITY. |
53 Minor INCOMPATIBILITY. |