src/HOL/Import/HOL4Setup.thy
changeset 17322 781abf7011e6
parent 16417 9bc16273c2d4
child 17801 30cbd2685e73
     1.1 --- a/src/HOL/Import/HOL4Setup.thy	Mon Sep 12 12:11:17 2005 +0200
     1.2 +++ b/src/HOL/Import/HOL4Setup.thy	Mon Sep 12 15:52:00 2005 +0200
     1.3 @@ -24,19 +24,18 @@
     1.4  
     1.5  defs
     1.6    ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"
     1.7 -  ONTO_DEF   : "ONTO f == ALL y. EX x. y = f x"
     1.8  
     1.9  lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV"
    1.10    by (simp add: ONE_ONE_DEF inj_on_def)
    1.11  
    1.12 -lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(ONTO f))"
    1.13 +lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(surj f))"
    1.14  proof (rule exI,safe)
    1.15    show "inj Suc_Rep"
    1.16      by (rule inj_Suc_Rep)
    1.17  next
    1.18 -  assume "ONTO Suc_Rep"
    1.19 +  assume "surj Suc_Rep"
    1.20    hence "ALL y. EX x. y = Suc_Rep x"
    1.21 -    by (simp add: ONTO_DEF surj_def)
    1.22 +    by (simp add: surj_def)
    1.23    hence "EX x. Zero_Rep = Suc_Rep x"
    1.24      by (rule spec)
    1.25    thus False