| changeset 11003 | ee0838d89deb |
| parent 10231 | 178a272bceeb |
| child 11034 | 568eb11f8d52 |
--- a/src/HOL/simpdata.ML Tue Jan 30 18:53:46 2001 +0100 +++ b/src/HOL/simpdata.ML Tue Jan 30 18:57:24 2001 +0100 @@ -233,6 +233,8 @@ bind_thms ("if_splits", [split_if, split_if_asm]); +bind_thm ("if_def2", read_instantiate [("P","\\<lambda>x. x")] split_if); + Goal "(if c then x else x) = x"; by (stac split_if 1); by (Blast_tac 1);