equal
deleted
inserted
replaced
466 by (REPEAT (etac allE 1)); |
466 by (REPEAT (etac allE 1)); |
467 by (rtac (some1_equality RS sym) 1); |
467 by (rtac (some1_equality RS sym) 1); |
468 by (atac 1); |
468 by (atac 1); |
469 by (atac 1); |
469 by (atac 1); |
470 qed "fun_rel_comp_unique"; |
470 qed "fun_rel_comp_unique"; |
|
471 |
|
472 |
|
473 section "inverse image"; |
|
474 |
|
475 Goalw [trans_def,inv_image_def] |
|
476 "!!r. trans r ==> trans (inv_image r f)"; |
|
477 by (Simp_tac 1); |
|
478 by (Blast_tac 1); |
|
479 qed "trans_inv_image"; |
|
480 |