# HG changeset patch
# User wenzelm
# Date 963947337 -7200
# Node ID 6e1ac1629ac7927cb4e04f411ba358c7206618a3
# Parent  8e8941c491e694f40c5b357080b2326919fe83d9
removed obsolete expand_if = split_if;

diff -r 8e8941c491e6 -r 6e1ac1629ac7 src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Tue Jul 18 21:08:40 2000 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Tue Jul 18 21:08:57 2000 +0200
@@ -246,7 +246,7 @@
            fast_tac (claset() addEs [Cast_conf])] 8);
 
 (* 7 LAss *)
-by( asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by( asm_simp_tac (simpset() addsplits [split_if]) 1);
 by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac] 1);
 by( blast_tac (claset() addIs [conforms_upd_local, conf_widen]) 1);
 
diff -r 8e8941c491e6 -r 6e1ac1629ac7 src/HOL/MicroJava/J/State.ML
--- a/src/HOL/MicroJava/J/State.ML	Tue Jul 18 21:08:40 2000 +0200
+++ b/src/HOL/MicroJava/J/State.ML	Tue Jul 18 21:08:57 2000 +0200
@@ -19,7 +19,7 @@
 
 val raise_if_True = prove_goalw thy [raise_if_def] 
 	"raise_if True x y \\<noteq> None"
-(K [split_tac [expand_if] 1,Auto_tac]);
+(K [split_tac [split_if] 1,Auto_tac]);
 
 val raise_if_False = prove_goalw thy [raise_if_def] 
 	"raise_if False x y = y"
@@ -41,20 +41,20 @@
 
 val raise_if_SomeD = prove_goalw thy [raise_if_def] 
 	"raise_if c x y = Some z \\<longrightarrow> c \\<and>  Some z = Some x |  y = Some z" 
-(K [split_tac [expand_if] 1,Auto_tac]) RS mp;
+(K [split_tac [split_if] 1,Auto_tac]) RS mp;
 
 val raise_if_NoneD = prove_goalw thy [raise_if_def] 
 	"raise_if c x y = None \\<longrightarrow> \\<not> c \\<and>  y = None"
-(K [split_tac [expand_if] 1,Auto_tac]) RS mp;
+(K [split_tac [split_if] 1,Auto_tac]) RS mp;
 
 
 val np_NoneD = (prove_goalw thy [np_def, raise_if_def] 
 	"np a' x' = None \\<longrightarrow> x' = None \\<and>  a' \\<noteq> Null" (fn _ => [
-	split_tac [expand_if] 1,
+	split_tac [split_if] 1,
 	Auto_tac ])) RS mp;
 val np_None = (prove_goalw thy [np_def, raise_if_def] 
 	"a' \\<noteq> Null \\<longrightarrow> np a' x' = x'" (fn _ => [
-	split_tac [expand_if] 1,
+	split_tac [split_if] 1,
 	Auto_tac ])) RS mp;
 val np_Some = prove_goalw thy [np_def, raise_if_def] "np a' (Some xc) = Some xc"
 	(fn _ => [Auto_tac ]);
diff -r 8e8941c491e6 -r 6e1ac1629ac7 src/HOL/Real/Hyperreal/HyperDef.ML
--- a/src/HOL/Real/Hyperreal/HyperDef.ML	Tue Jul 18 21:08:40 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Tue Jul 18 21:08:57 2000 +0200
@@ -346,7 +346,7 @@
 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
 by (rotate_tac 1 1);
 by (asm_full_simp_tac (simpset() addsimps 
-    [hypreal_hrinv,hypreal_zero_def] setloop (split_tac [expand_if])) 1);
+    [hypreal_hrinv,hypreal_zero_def] addsplits [split_if]) 1);
 by (ultra_tac (claset() addDs (map (rename_numerals thy)
 			       [rinv_not_zero,real_rinv_rinv]),
 	       simpset()) 1);
diff -r 8e8941c491e6 -r 6e1ac1629ac7 src/HOL/Real/Hyperreal/Zorn.ML
--- a/src/HOL/Real/Hyperreal/Zorn.ML	Tue Jul 18 21:08:40 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.ML	Tue Jul 18 21:08:57 2000 +0200
@@ -28,7 +28,7 @@
 
 (* increasingD2 of ZF/Zorn.ML *) 
 Goalw [succ_def] "x <= succ S x";
-by (rtac (expand_if RS iffD2) 1);
+by (rtac (split_if RS iffD2) 1);
 by (auto_tac (claset(),simpset() addsimps [super_def,
                maxchain_def,psubset_def]));
 by (rtac swap 1 THEN assume_tac 1);
@@ -190,7 +190,7 @@
 by (etac TFin_induct 1);
 by (asm_simp_tac (simpset() addsimps [succ_def,
     select_super RS (super_subset_chain RS subsetD)]
-                   setloop split_tac [expand_if]) 1);
+                   addsplits [split_if]) 1);
 by (rewtac chain_def);
 by (rtac CollectI 1);
 by Safe_tac;
diff -r 8e8941c491e6 -r 6e1ac1629ac7 src/HOLCF/IOA/meta_theory/TLS.ML
--- a/src/HOLCF/IOA/meta_theory/TLS.ML	Tue Jul 18 21:08:40 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Tue Jul 18 21:08:57 2000 +0200
@@ -91,7 +91,7 @@
 \             .--> (Next (Init (%(s,a,t).Q s))))";
 
 by (clarify_tac set_cs 1);
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (asm_full_simp_tac (simpset() addsplits [split_if]) 1);
 (* TL = UU *)
 by (rtac conjI 1);
 by (pair_tac "ex" 1);