| author | paulson |
| Wed, 11 Nov 1998 15:49:15 +0100 | |
| changeset 5847 | 17c869f24c5f |
| parent 5846 | d99feda2d226 |
| child 5848 | 99dea3c24efb |
| src/HOL/Fun.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Fun.ML Wed Nov 11 15:45:32 1998 +0100 +++ b/src/HOL/Fun.ML Wed Nov 11 15:49:15 1998 +0100 @@ -180,6 +180,12 @@ qed "image_set_diff"; + +val [major] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; +by (blast_tac (claset() addIs [major RS sym]) 1); +qed "surjI"; + + val set_cs = claset() delrules [equalityI];