Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mod by Norber Voelcker
authornipkow
Wed, 21 Jul 1999 11:34:59 +0200
changeset 7051 9b6bdced3dc6
parent 7050 c70d3402fef5
child 7052 4c201f27c74e
Mod by Norber Voelcker
src/HOL/Fun.ML file | annotate | diff | comparison | revisions 
--- 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";
isabelle