equal
deleted
inserted
replaced
54 val csum_Cnotzero2 = @{thm csum_Cnotzero2}; |
54 val csum_Cnotzero2 = @{thm csum_Cnotzero2}; |
55 val ctwo_Cnotzero = @{thm ctwo_Cnotzero}; |
55 val ctwo_Cnotzero = @{thm ctwo_Cnotzero}; |
56 val o_eq_dest_lhs = @{thm o_eq_dest_lhs}; |
56 val o_eq_dest_lhs = @{thm o_eq_dest_lhs}; |
57 val ordIso_transitive = @{thm ordIso_transitive}; |
57 val ordIso_transitive = @{thm ordIso_transitive}; |
58 val ordLeq_csum2 = @{thm ordLeq_csum2}; |
58 val ordLeq_csum2 = @{thm ordLeq_csum2}; |
59 val subset_UNIV = @{thm subset_UNIV}; |
|
60 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]}; |
59 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]}; |
61 val trans_o_apply = @{thm trans[OF o_apply]}; |
60 val trans_o_apply = @{thm trans[OF o_apply]}; |
62 |
61 |
63 |
62 |
64 |
63 |