equal
deleted
inserted
replaced
71 val diagI = thm "diagI"; |
71 val diagI = thm "diagI"; |
72 val diag_def = thm "diag_def"; |
72 val diag_def = thm "diag_def"; |
73 val diag_eqI = thm "diag_eqI"; |
73 val diag_eqI = thm "diag_eqI"; |
74 val diag_iff = thm "diag_iff"; |
74 val diag_iff = thm "diag_iff"; |
75 val diag_subset_Times = thm "diag_subset_Times"; |
75 val diag_subset_Times = thm "diag_subset_Times"; |
76 val fun_rel_comp_def = thm "fun_rel_comp_def"; |
|
77 val fun_rel_comp_mono = thm "fun_rel_comp_mono"; |
|
78 val fun_rel_comp_unique = thm "fun_rel_comp_unique"; |
|
79 val inv_image_def = thm "inv_image_def"; |
76 val inv_image_def = thm "inv_image_def"; |
80 val pair_in_Id_conv = thm "pair_in_Id_conv"; |
77 val pair_in_Id_conv = thm "pair_in_Id_conv"; |
81 val reflD = thm "reflD"; |
78 val reflD = thm "reflD"; |
82 val reflI = thm "reflI"; |
79 val reflI = thm "reflI"; |
83 val refl_converse = thm "refl_converse"; |
80 val refl_converse = thm "refl_converse"; |