addsplits [split_if];
authorwenzelm
Tue Jul 18 21:44:42 2000 +0200 (2000-07-18)
changeset 93873bab31b55a95
parent 9386 8800603d99f6
child 9388 0b039a3575eb
addsplits [split_if];
src/HOL/Real/Hyperreal/HyperDef.ML
     1.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Tue Jul 18 21:09:18 2000 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Tue Jul 18 21:44:42 2000 +0200
     1.3 @@ -357,7 +357,7 @@
     1.4  Goalw [hypreal_one_def] "hrinv(1hr) = 1hr";
     1.5  by (full_simp_tac (simpset() addsimps [hypreal_hrinv,
     1.6         real_zero_not_eq_one RS not_sym] 
     1.7 -                   setloop (split_tac [expand_if])) 1);
     1.8 +                   addsplits [split_if]) 1);
     1.9  qed "hypreal_hrinv_1";
    1.10  Addsimps [hypreal_hrinv_1];
    1.11  
    1.12 @@ -648,7 +648,7 @@
    1.13  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    1.14  by (rotate_tac 1 1);
    1.15  by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
    1.16 -    hypreal_mult] setloop (split_tac [expand_if])) 1);
    1.17 +    hypreal_mult] addsplits [split_if]) 1);
    1.18  by (dtac FreeUltrafilterNat_Compl_mem 1);
    1.19  by (blast_tac (claset() addSIs [real_mult_inv_right,
    1.20      FreeUltrafilterNat_subset]) 1);
    1.21 @@ -712,7 +712,7 @@
    1.22  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    1.23  by (rotate_tac 1 1);
    1.24  by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
    1.25 -    hypreal_mult] setloop (split_tac [expand_if])) 1);
    1.26 +    hypreal_mult] addsplits [split_if]) 1);
    1.27  by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
    1.28  by (ultra_tac (claset() addIs [ccontr]
    1.29                          addDs [rename_numerals thy rinv_not_zero],
    1.30 @@ -1802,7 +1802,7 @@
    1.31  Goal "ehr = hrinv(whr)";
    1.32  by (asm_full_simp_tac (simpset() addsimps 
    1.33      [hypreal_hrinv,omega_def,epsilon_def]
    1.34 -    setloop (split_tac [expand_if])) 1);
    1.35 +    addsplits [split_if]) 1);
    1.36  qed "hypreal_epsilon_hrinv_omega";
    1.37  
    1.38  (*----------------------------------------------------------------