src/FOL/simpdata.ML
changeset 4325 e72cba5af6c5
parent 4203 ca73de799b73
child 4349 50403e5a44c0
     1.1 --- a/src/FOL/simpdata.ML	Fri Nov 28 10:52:32 1997 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Fri Nov 28 10:54:13 1997 +0100
     1.3 @@ -186,6 +186,8 @@
     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 +
     1.8 +
     1.9  (*** Standard simpsets ***)
    1.10  
    1.11  structure Induction = InductionFun(struct val spec=IFOL.spec end);
    1.12 @@ -202,6 +204,9 @@
    1.13  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
    1.14  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    1.15  
    1.16 +infix 4 addsplits;
    1.17 +fun ss addsplits splits = ss addloop (split_tac splits);
    1.18 +
    1.19  val IFOL_simps =
    1.20     [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
    1.21      imp_simps @ iff_simps @ quant_simps;