equal
deleted
inserted
replaced
107 by (Blast_tac 1); |
107 by (Blast_tac 1); |
108 qed "inverse_inverse"; |
108 qed "inverse_inverse"; |
109 Addsimps [inverse_inverse]; |
109 Addsimps [inverse_inverse]; |
110 |
110 |
111 goal Relation.thy "(r O s)^-1 = s^-1 O r^-1"; |
111 goal Relation.thy "(r O s)^-1 = s^-1 O r^-1"; |
112 by(Blast_tac 1); |
112 by (Blast_tac 1); |
113 qed "inverse_comp"; |
113 qed "inverse_comp"; |
114 |
114 |
115 (** Domain **) |
115 (** Domain **) |
116 |
116 |
117 qed_goalw "Domain_iff" Relation.thy [Domain_def] |
117 qed_goalw "Domain_iff" Relation.thy [Domain_def] |