src/HOL/Real/Hyperreal/SEQ.ML
changeset 10721 12b166418455
parent 10720 1ce5a189f672
equal deleted inserted replaced
10720:1ce5a189f672 10721:12b166418455
  1038 by (Step_tac 1);
  1038 by (Step_tac 1);
  1039 by (dtac starfun_le_mono 1);
  1039 by (dtac starfun_le_mono 1);
  1040 by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
  1040 by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
  1041 by (dres_inst_tac [("x","whn")] spec 1);
  1041 by (dres_inst_tac [("x","whn")] spec 1);
  1042 by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
  1042 by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
       
  1043 by Auto_tac;
  1043 by (auto_tac (claset() addIs 
  1044 by (auto_tac (claset() addIs 
  1044     [hypreal_of_real_le_add_Infininitesimal_cancel2], simpset()));
  1045     [hypreal_of_real_le_add_Infininitesimal_cancel2], simpset()));
  1045 qed "NSLIMSEQ_le";
  1046 qed "NSLIMSEQ_le";
  1046 
  1047 
  1047 (* standard version *)
  1048 (* standard version *)