src/HOL/simpdata.ML
changeset 4681 a331c1f5a23e
parent 4677 c4b07b8579fd
child 4718 fc2ba9fb2135
     1.1 --- a/src/HOL/simpdata.ML	Thu Mar 05 10:47:27 1998 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Fri Mar 06 15:19:29 1998 +0100
     1.3 @@ -334,13 +334,23 @@
     1.4  val split_asm_tac = mk_case_split_asm_tac split_tac 
     1.5  			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
     1.6  
     1.7 -infix 4 addsplits;
     1.8 +infix 4 addsplits delsplits;
     1.9 +
    1.10  fun ss addsplits splits =
    1.11    let fun addsplit(ss,split) =
    1.12          let val name = "split " ^ const_of_split_thm split
    1.13          in ss addloop (name,split_tac [split]) end
    1.14    in foldl addsplit (ss,splits) end;
    1.15  
    1.16 +fun ss delsplits splits =
    1.17 +  let fun delsplit(ss,split) =
    1.18 +        let val name = "split " ^ const_of_split_thm split
    1.19 +        in ss delloop name end
    1.20 +  in foldl delsplit (ss,splits) end;
    1.21 +
    1.22 +fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
    1.23 +fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
    1.24 +
    1.25  qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
    1.26    (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
    1.27  
    1.28 @@ -385,7 +395,8 @@
    1.29  			    setSSolver   safe_solver
    1.30  			    setSolver  unsafe_solver
    1.31  			    setmksimps (mksimps mksimps_pairs)
    1.32 -			    setmkeqTrue mk_meta_eq_True;
    1.33 +			    setmkeqTrue mk_meta_eq_True
    1.34 +                            addsplits [expand_if];
    1.35  
    1.36  val HOL_ss = 
    1.37      HOL_basic_ss addsimps