# HG changeset patch
# User paulson
# Date 990449610 -7200
# Node ID 92eddd0914a9d4d141823c06f2046e1c1dc83092
# Parent  6a20952757b29b0b8512799273ae0c1629598d7a
if_splits and split_if_asm

diff -r 6a20952757b2 -r 92eddd0914a9 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Mon May 21 14:53:11 2001 +0200
+++ b/src/ZF/simpdata.ML	Mon May 21 14:53:30 2001 +0200
@@ -117,6 +117,14 @@
 		           addsplits [split_if]
                            setSolver (mk_solver "types" Type_solver_tac);
 
+(** Splitting IFs in the assumptions **)
+
+Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))";
+by (Simp_tac 1); 
+qed "split_if_asm";   
+
+bind_thms ("if_splits", [split_if, split_if_asm]);
+
 (** One-point rule for bounded quantifiers: see HOL/Set.ML **)
 
 Goal "(EX x:A. x=a) <-> (a:A)";