--- 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)";