# HG changeset patch
# User paulson
# Date 880710853 -3600
# Node ID e72cba5af6c57002773c2a0dd01611c78c44a5fc
# Parent  9bfac4684f2f8362a5a77eeb1d8beb431070741f
addsplits now in FOL, ZF too

diff -r 9bfac4684f2f -r e72cba5af6c5 NEWS
--- a/NEWS	Fri Nov 28 10:52:32 1997 +0100
+++ b/NEWS	Fri Nov 28 10:54:13 1997 +0100
@@ -89,6 +89,10 @@
 
 * added prems argument to simplification procedures;
 
+* HOL, FOL, ZF: added infix function `addsplits':
+  instead of `<simpset> setloop (split_tac <thms>)'
+  you can simply write `<simpset> addsplits <thms>'
+
 
 *** Syntax ***
 
@@ -113,16 +117,12 @@
 
 * HOL/Map: new theory of `maps' a la VDM;
 
-* HOL/simplifier: added infix function `addsplits':
-  instead of `<simpset> setloop (split_tac <thms>)'
-  you can simply write `<simpset> addsplits <thms>'
-
 * HOL/simplifier: terms of the form
-  `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)
+  `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)'  (or t=x)
   are rewritten to
   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',
   and those of the form
-  `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)' (or t=x)
+  `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)'  (or t=x)
   are rewritten to
   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',
 
diff -r 9bfac4684f2f -r e72cba5af6c5 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Nov 28 10:52:32 1997 +0100
+++ b/src/FOL/simpdata.ML	Fri Nov 28 10:54:13 1997 +0100
@@ -186,6 +186,8 @@
 val split_asm_tac = mk_case_split_asm_tac split_tac 
 			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
 
+
+
 (*** Standard simpsets ***)
 
 structure Induction = InductionFun(struct val spec=IFOL.spec end);
@@ -202,6 +204,9 @@
 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
 
+infix 4 addsplits;
+fun ss addsplits splits = ss addloop (split_tac splits);
+
 val IFOL_simps =
    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
     imp_simps @ iff_simps @ quant_simps;