src/HOL/simpdata.ML
changeset 9384 8e8941c491e6
parent 9164 88e0f647b9c2
child 9511 bb029080ff8b
     1.1 --- a/src/HOL/simpdata.ML	Tue Jul 18 21:08:20 2000 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Tue Jul 18 21:08:40 2000 +0200
     1.3 @@ -293,14 +293,13 @@
     1.4  by (ALLGOALS (Blast_tac));
     1.5  qed "split_if";
     1.6  
     1.7 -(* for backwards compatibility: *)
     1.8 -val expand_if = split_if;
     1.9 -
    1.10  Goal "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))";
    1.11  by (stac split_if 1);
    1.12  by (Blast_tac 1);
    1.13  qed "split_if_asm";
    1.14  
    1.15 +bind_thms ("if_splits", [split_if, split_if_asm]);
    1.16 +
    1.17  Goal "(if c then x else x) = x";
    1.18  by (stac split_if 1);
    1.19  by (Blast_tac 1);