* HOL: removed obsolete expand_if = split_if; theorems if_splits =
split_if split_if_asm;
--- a/src/HOL/simpdata.ML Tue Jul 18 21:08:20 2000 +0200
+++ b/src/HOL/simpdata.ML Tue Jul 18 21:08:40 2000 +0200
@@ -293,14 +293,13 @@
by (ALLGOALS (Blast_tac));
qed "split_if";
-(* for backwards compatibility: *)
-val expand_if = split_if;
-
Goal "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))";
by (stac split_if 1);
by (Blast_tac 1);
qed "split_if_asm";
+bind_thms ("if_splits", [split_if, split_if_asm]);
+
Goal "(if c then x else x) = x";
by (stac split_if 1);
by (Blast_tac 1);