src/HOL/Real/Hyperreal/HyperDef.ML
changeset 7499 23e090051cb8
parent 7322 d16d7ddcc842
child 7825 1be9b63e7d93
     1.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Mon Sep 06 22:12:08 1999 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Tue Sep 07 10:40:58 1999 +0200
     1.3 @@ -1096,7 +1096,7 @@
     1.4  by (dtac (hypreal_minus_zero_less_iff RS iffD2) 2);
     1.5  by (dres_inst_tac [("R2.0","-x")] hypreal_less_trans 2);
     1.6  by (Auto_tac );
     1.7 -by (forward_tac [hypreal_add_order] 1 THEN assume_tac 1);
     1.8 +by (ftac hypreal_add_order 1 THEN assume_tac 1);
     1.9  by (dres_inst_tac [("C","-x"),("B","x + x")] hypreal_add_less_mono1 1);
    1.10  by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
    1.11  qed "hypreal_gt_zero_iff";
    1.12 @@ -1318,7 +1318,7 @@
    1.13  qed "hypreal_hrinv_gt_zero";
    1.14  
    1.15  Goal "x < 0hr ==> hrinv x < 0hr";
    1.16 -by (forward_tac [hypreal_not_refl2] 1);
    1.17 +by (ftac hypreal_not_refl2 1);
    1.18  by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
    1.19  by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
    1.20  by (dtac (hypreal_minus_hrinv RS sym) 1);
    1.21 @@ -1394,13 +1394,13 @@
    1.22  
    1.23  (* TODO: remove redundant  0hr < x *)
    1.24  Goal "[| 0hr < r; 0hr < x; r < x |] ==> hrinv x < hrinv r";
    1.25 -by (forward_tac [hypreal_hrinv_gt_zero] 1);
    1.26 +by (ftac hypreal_hrinv_gt_zero 1);
    1.27  by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1);
    1.28  by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1);
    1.29  by (assume_tac 1);
    1.30  by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
    1.31           not_sym RS hypreal_mult_hrinv]) 1);
    1.32 -by (forward_tac [hypreal_hrinv_gt_zero] 1);
    1.33 +by (ftac hypreal_hrinv_gt_zero 1);
    1.34  by (forw_inst_tac [("x","1hr"),("z","hrinv x")] hypreal_mult_less_mono2 1);
    1.35  by (assume_tac 1);
    1.36  by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS