# HG changeset patch
# User wenzelm
# Date 963949482 -7200
# Node ID 3bab31b55a951f32403e20d38fcc4885ada28579
# Parent  8800603d99f6b3abd30392f72ab0dee059e30864
addsplits [split_if];

diff -r 8800603d99f6 -r 3bab31b55a95 src/HOL/Real/Hyperreal/HyperDef.ML
--- a/src/HOL/Real/Hyperreal/HyperDef.ML	Tue Jul 18 21:09:18 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Tue Jul 18 21:44:42 2000 +0200
@@ -357,7 +357,7 @@
 Goalw [hypreal_one_def] "hrinv(1hr) = 1hr";
 by (full_simp_tac (simpset() addsimps [hypreal_hrinv,
        real_zero_not_eq_one RS not_sym] 
-                   setloop (split_tac [expand_if])) 1);
+                   addsplits [split_if]) 1);
 qed "hypreal_hrinv_1";
 Addsimps [hypreal_hrinv_1];
 
@@ -648,7 +648,7 @@
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (rotate_tac 1 1);
 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
-    hypreal_mult] setloop (split_tac [expand_if])) 1);
+    hypreal_mult] addsplits [split_if]) 1);
 by (dtac FreeUltrafilterNat_Compl_mem 1);
 by (blast_tac (claset() addSIs [real_mult_inv_right,
     FreeUltrafilterNat_subset]) 1);
@@ -712,7 +712,7 @@
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (rotate_tac 1 1);
 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
-    hypreal_mult] setloop (split_tac [expand_if])) 1);
+    hypreal_mult] addsplits [split_if]) 1);
 by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
 by (ultra_tac (claset() addIs [ccontr]
                         addDs [rename_numerals thy rinv_not_zero],
@@ -1802,7 +1802,7 @@
 Goal "ehr = hrinv(whr)";
 by (asm_full_simp_tac (simpset() addsimps 
     [hypreal_hrinv,omega_def,epsilon_def]
-    setloop (split_tac [expand_if])) 1);
+    addsplits [split_if]) 1);
 qed "hypreal_epsilon_hrinv_omega";
 
 (*----------------------------------------------------------------