equal
deleted
inserted
replaced
77 preorder.antisymp_greater[simp] |
77 preorder.antisymp_greater[simp] |
78 preorder.antisymp_less[simp] |
78 preorder.antisymp_less[simp] |
79 preorder.reflp_on_ge[simp] |
79 preorder.reflp_on_ge[simp] |
80 preorder.reflp_on_le[simp] |
80 preorder.reflp_on_le[simp] |
81 reflp_on_conversp[simp] |
81 reflp_on_conversp[simp] |
|
82 symp_on_sym_on_eq[pred_set_conv] |
82 totalI |
83 totalI |
83 totalp_on_converse[simp] |
84 totalp_on_converse[simp] |
84 totalp_on_singleton[simp] |
85 totalp_on_singleton[simp] |
85 |
86 |
86 * Theory "HOL.Transitive_Closure": |
87 * Theory "HOL.Transitive_Closure": |