equal
deleted
inserted
replaced
178 Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B"; |
178 Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B"; |
179 by (Blast_tac 1); |
179 by (Blast_tac 1); |
180 qed "image_set_diff"; |
180 qed "image_set_diff"; |
181 |
181 |
182 |
182 |
|
183 |
|
184 val [major] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; |
|
185 by (blast_tac (claset() addIs [major RS sym]) 1); |
|
186 qed "surjI"; |
|
187 |
|
188 |
183 val set_cs = claset() delrules [equalityI]; |
189 val set_cs = claset() delrules [equalityI]; |
184 |
190 |
185 |
191 |
186 section "fun_upd"; |
192 section "fun_upd"; |
187 |
193 |