equal
deleted
inserted
replaced
98 @{thm[display] image_Un[no_vars]} |
98 @{thm[display] image_Un[no_vars]} |
99 \rulename{image_Un} |
99 \rulename{image_Un} |
100 *} |
100 *} |
101 |
101 |
102 text{* |
102 text{* |
103 @{thm[display] image_compose[no_vars]} |
103 @{thm[display] image_comp[no_vars]} |
104 \rulename{image_compose} |
104 \rulename{image_comp} |
105 |
105 |
106 @{thm[display] image_Int[no_vars]} |
106 @{thm[display] image_Int[no_vars]} |
107 \rulename{image_Int} |
107 \rulename{image_Int} |
108 |
108 |
109 @{thm[display] bij_image_Compl_eq[no_vars]} |
109 @{thm[display] bij_image_Compl_eq[no_vars]} |