removed obsolete expand_if = split_if;
authorwenzelm
Tue Jul 18 21:08:57 2000 +0200 (2000-07-18)
changeset 93856e1ac1629ac7
parent 9384 8e8941c491e6
child 9386 8800603d99f6
removed obsolete expand_if = split_if;
src/HOL/MicroJava/J/JTypeSafe.ML
src/HOL/MicroJava/J/State.ML
src/HOL/Real/Hyperreal/HyperDef.ML
src/HOL/Real/Hyperreal/Zorn.ML
src/HOLCF/IOA/meta_theory/TLS.ML
     1.1 --- a/src/HOL/MicroJava/J/JTypeSafe.ML	Tue Jul 18 21:08:40 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Tue Jul 18 21:08:57 2000 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4             fast_tac (claset() addEs [Cast_conf])] 8);
     1.5  
     1.6  (* 7 LAss *)
     1.7 -by( asm_simp_tac (simpset() addsplits [expand_if]) 1);
     1.8 +by( asm_simp_tac (simpset() addsplits [split_if]) 1);
     1.9  by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac] 1);
    1.10  by( blast_tac (claset() addIs [conforms_upd_local, conf_widen]) 1);
    1.11  
     2.1 --- a/src/HOL/MicroJava/J/State.ML	Tue Jul 18 21:08:40 2000 +0200
     2.2 +++ b/src/HOL/MicroJava/J/State.ML	Tue Jul 18 21:08:57 2000 +0200
     2.3 @@ -19,7 +19,7 @@
     2.4  
     2.5  val raise_if_True = prove_goalw thy [raise_if_def] 
     2.6  	"raise_if True x y \\<noteq> None"
     2.7 -(K [split_tac [expand_if] 1,Auto_tac]);
     2.8 +(K [split_tac [split_if] 1,Auto_tac]);
     2.9  
    2.10  val raise_if_False = prove_goalw thy [raise_if_def] 
    2.11  	"raise_if False x y = y"
    2.12 @@ -41,20 +41,20 @@
    2.13  
    2.14  val raise_if_SomeD = prove_goalw thy [raise_if_def] 
    2.15  	"raise_if c x y = Some z \\<longrightarrow> c \\<and>  Some z = Some x |  y = Some z" 
    2.16 -(K [split_tac [expand_if] 1,Auto_tac]) RS mp;
    2.17 +(K [split_tac [split_if] 1,Auto_tac]) RS mp;
    2.18  
    2.19  val raise_if_NoneD = prove_goalw thy [raise_if_def] 
    2.20  	"raise_if c x y = None \\<longrightarrow> \\<not> c \\<and>  y = None"
    2.21 -(K [split_tac [expand_if] 1,Auto_tac]) RS mp;
    2.22 +(K [split_tac [split_if] 1,Auto_tac]) RS mp;
    2.23  
    2.24  
    2.25  val np_NoneD = (prove_goalw thy [np_def, raise_if_def] 
    2.26  	"np a' x' = None \\<longrightarrow> x' = None \\<and>  a' \\<noteq> Null" (fn _ => [
    2.27 -	split_tac [expand_if] 1,
    2.28 +	split_tac [split_if] 1,
    2.29  	Auto_tac ])) RS mp;
    2.30  val np_None = (prove_goalw thy [np_def, raise_if_def] 
    2.31  	"a' \\<noteq> Null \\<longrightarrow> np a' x' = x'" (fn _ => [
    2.32 -	split_tac [expand_if] 1,
    2.33 +	split_tac [split_if] 1,
    2.34  	Auto_tac ])) RS mp;
    2.35  val np_Some = prove_goalw thy [np_def, raise_if_def] "np a' (Some xc) = Some xc"
    2.36  	(fn _ => [Auto_tac ]);
     3.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Tue Jul 18 21:08:40 2000 +0200
     3.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Tue Jul 18 21:08:57 2000 +0200
     3.3 @@ -346,7 +346,7 @@
     3.4  by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
     3.5  by (rotate_tac 1 1);
     3.6  by (asm_full_simp_tac (simpset() addsimps 
     3.7 -    [hypreal_hrinv,hypreal_zero_def] setloop (split_tac [expand_if])) 1);
     3.8 +    [hypreal_hrinv,hypreal_zero_def] addsplits [split_if]) 1);
     3.9  by (ultra_tac (claset() addDs (map (rename_numerals thy)
    3.10  			       [rinv_not_zero,real_rinv_rinv]),
    3.11  	       simpset()) 1);
     4.1 --- a/src/HOL/Real/Hyperreal/Zorn.ML	Tue Jul 18 21:08:40 2000 +0200
     4.2 +++ b/src/HOL/Real/Hyperreal/Zorn.ML	Tue Jul 18 21:08:57 2000 +0200
     4.3 @@ -28,7 +28,7 @@
     4.4  
     4.5  (* increasingD2 of ZF/Zorn.ML *) 
     4.6  Goalw [succ_def] "x <= succ S x";
     4.7 -by (rtac (expand_if RS iffD2) 1);
     4.8 +by (rtac (split_if RS iffD2) 1);
     4.9  by (auto_tac (claset(),simpset() addsimps [super_def,
    4.10                 maxchain_def,psubset_def]));
    4.11  by (rtac swap 1 THEN assume_tac 1);
    4.12 @@ -190,7 +190,7 @@
    4.13  by (etac TFin_induct 1);
    4.14  by (asm_simp_tac (simpset() addsimps [succ_def,
    4.15      select_super RS (super_subset_chain RS subsetD)]
    4.16 -                   setloop split_tac [expand_if]) 1);
    4.17 +                   addsplits [split_if]) 1);
    4.18  by (rewtac chain_def);
    4.19  by (rtac CollectI 1);
    4.20  by Safe_tac;
     5.1 --- a/src/HOLCF/IOA/meta_theory/TLS.ML	Tue Jul 18 21:08:40 2000 +0200
     5.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Tue Jul 18 21:08:57 2000 +0200
     5.3 @@ -91,7 +91,7 @@
     5.4  \             .--> (Next (Init (%(s,a,t).Q s))))";
     5.5  
     5.6  by (clarify_tac set_cs 1);
     5.7 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
     5.8 +by (asm_full_simp_tac (simpset() addsplits [split_if]) 1);
     5.9  (* TL = UU *)
    5.10  by (rtac conjI 1);
    5.11  by (pair_tac "ex" 1);