* HOL: removed obsolete expand_if = split_if; theorems if_splits =
authorwenzelm
Tue Jul 18 21:08:40 2000 +0200 (2000-07-18)
changeset 93848e8941c491e6
parent 9383 c21fa1c48de0
child 9385 6e1ac1629ac7
* HOL: removed obsolete expand_if = split_if; theorems if_splits =
split_if split_if_asm;
src/HOL/simpdata.ML
     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);