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