| changeset 7051 | 9b6bdced3dc6 |
| parent 7014 | 11ee650edcd2 |
| child 7089 | 9bfb8e218b99 |
--- a/src/HOL/Fun.ML Tue Jul 20 18:50:46 1999 +0200 +++ b/src/HOL/Fun.ML Wed Jul 21 11:34:59 1999 +0200 @@ -174,7 +174,7 @@ (*** Lemmas about injective functions and inv ***) -Goalw [o_def] "[| inj_on f A; inj_on g (range f) |] ==> inj_on (g o f) A"; +Goalw [o_def] "[| inj_on f A; inj_on g (f``A) |] ==> inj_on (g o f) A"; by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1); qed "comp_inj_on";