src/HOL/Real/Hyperreal/HyperDef.ML
changeset 7825 1be9b63e7d93
parent 7499 23e090051cb8
child 8856 435187ffc64e
     1.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Mon Oct 11 10:51:24 1999 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Mon Oct 11 10:52:51 1999 +0200
     1.3 @@ -1848,7 +1848,7 @@
     1.4  Goal "inj hypreal_of_nat";
     1.5  by (rtac injI 1);
     1.6  by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
     1.7 -        simpset() addsimps [hypreal_of_nat_iff,
     1.8 +        simpset() addsimps [split_if_mem1, hypreal_of_nat_iff,
     1.9          real_add_right_cancel,inj_real_of_nat RS injD]));
    1.10  qed "inj_hypreal_of_nat";
    1.11