| changeset 8156 | 33d23d0a300e |
| parent 8138 | 1e4cb069b19d |
| child 8173 | a9966d5ab84d |
--- a/src/HOL/Fun.ML Fri Jan 28 14:07:33 2000 +0100 +++ b/src/HOL/Fun.ML Fri Jan 28 14:07:53 2000 +0100 @@ -169,6 +169,11 @@ by (Blast_tac 1); qed "inj_on_contraD"; +Goal "inj (%s. {s})"; +br injI 1; +be singleton_inject 1; +qed "inj_singleton"; + Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A"; by (Blast_tac 1); qed "subset_inj_on";