equal
deleted
inserted
replaced
37 (* ********************************************************************** *) |
37 (* ********************************************************************** *) |
38 (* lemmas concerning FOL and pure ZF theory *) |
38 (* lemmas concerning FOL and pure ZF theory *) |
39 (* ********************************************************************** *) |
39 (* ********************************************************************** *) |
40 |
40 |
41 Goal "(A->X)=0 ==> X=0"; |
41 Goal "(A->X)=0 ==> X=0"; |
42 by (fast_tac (claset() addSIs [equals0I] addEs [lam_type RSN (2, equals0E)]) 1); |
42 by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 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 "[| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; A<=Df; A<=Dg |] ==> f``A=g``A"; |
47 Goal "[| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; A<=Df; A<=Dg |] ==> f``A=g``A"; |