src/HOL/Hyperreal/HyperNat.ML
changeset 11468 02cd5d5bc497
parent 10919 144ede948e58
child 11655 923e4d0d36d5
     1.1 --- a/src/HOL/Hyperreal/HyperNat.ML	Mon Aug 06 16:43:40 2001 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperNat.ML	Tue Aug 07 16:36:52 2001 +0200
     1.3 @@ -682,7 +682,7 @@
     1.4  Goalw [hypnat_one_def,hypnat_zero_def,hypnat_less_def] 
     1.5        "(0::hypnat) < 1hn";
     1.6  by (res_inst_tac [("x","%n. 0")] exI 1);
     1.7 -by (res_inst_tac [("x","%n. 1")] exI 1);
     1.8 +by (res_inst_tac [("x","%n. 1'")] exI 1);
     1.9  by Auto_tac;
    1.10  qed "hypnat_zero_less_one";
    1.11  
    1.12 @@ -806,11 +806,11 @@
    1.13  by Auto_tac;
    1.14  qed "hypnat_of_nat_le_iff";
    1.15  
    1.16 -Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat  1 = 1hn";
    1.17 +Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat 1' = 1hn";
    1.18  by (Simp_tac 1);
    1.19  qed "hypnat_of_nat_one";
    1.20  
    1.21 -Goalw [hypnat_of_nat_def,hypnat_zero_def] "hypnat_of_nat  0 = 0";
    1.22 +Goalw [hypnat_of_nat_def,hypnat_zero_def] "hypnat_of_nat 0 = 0";
    1.23  by (Simp_tac 1);
    1.24  qed "hypnat_of_nat_zero";
    1.25  
    1.26 @@ -903,7 +903,7 @@
    1.27  qed "SHNat_hypnat_of_nat";
    1.28  Addsimps [SHNat_hypnat_of_nat];
    1.29  
    1.30 -Goal "hypnat_of_nat 1 : Nats";
    1.31 +Goal "hypnat_of_nat 1' : Nats";
    1.32  by (Simp_tac 1);
    1.33  qed "SHNat_hypnat_of_nat_one";
    1.34