| changeset 9384 | 8e8941c491e6 |
| parent 9164 | 88e0f647b9c2 |
| child 9511 | bb029080ff8b |
--- 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);