src/ZF/simpdata.ML
changeset 11323 92eddd0914a9
parent 11233 34c81a796ee3
child 11695 8c66866fb0ff
     1.1 --- a/src/ZF/simpdata.ML	Mon May 21 14:53:11 2001 +0200
     1.2 +++ b/src/ZF/simpdata.ML	Mon May 21 14:53:30 2001 +0200
     1.3 @@ -117,6 +117,14 @@
     1.4  		           addsplits [split_if]
     1.5                             setSolver (mk_solver "types" Type_solver_tac);
     1.6  
     1.7 +(** Splitting IFs in the assumptions **)
     1.8 +
     1.9 +Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))";
    1.10 +by (Simp_tac 1); 
    1.11 +qed "split_if_asm";   
    1.12 +
    1.13 +bind_thms ("if_splits", [split_if, split_if_asm]);
    1.14 +
    1.15  (** One-point rule for bounded quantifiers: see HOL/Set.ML **)
    1.16  
    1.17  Goal "(EX x:A. x=a) <-> (a:A)";