equal
deleted
inserted
replaced
42 by (fast_tac (claset() addSIs [equals0I] addEs [lam_type RSN (2, equals0E)]) 1); |
42 by (fast_tac (claset() addSIs [equals0I] addEs [lam_type RSN (2, equals0E)]) 1); |
43 qed "fun_space_emptyD"; |
43 qed "fun_space_emptyD"; |
44 |
44 |
45 (* used only in WO1_DC.ML *) |
45 (* used only in WO1_DC.ML *) |
46 (*Note simpler proof*) |
46 (*Note simpler proof*) |
47 goal ZF.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; \ |
47 Goal "[| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; A<=Df; A<=Dg |] ==> f``A=g``A"; |
48 \ A<=Df; A<=Dg |] ==> f``A=g``A"; |
|
49 by (asm_simp_tac (simpset() addsimps [image_fun]) 1); |
48 by (asm_simp_tac (simpset() addsimps [image_fun]) 1); |
50 qed "images_eq"; |
49 qed "images_eq"; |
51 |
50 |
52 (* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) |
51 (* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) |
53 (*I don't know where to put this one.*) |
52 (*I don't know where to put this one.*) |