# HG changeset patch
# User wenzelm
# Date 963947320 -7200
# Node ID 8e8941c491e694f40c5b357080b2326919fe83d9
# Parent  c21fa1c48de0a2671a898d3a4e8f43e70101e7ac
* HOL: removed obsolete expand_if = split_if; theorems if_splits =
split_if split_if_asm;

diff -r c21fa1c48de0 -r 8e8941c491e6 src/HOL/simpdata.ML
--- 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);