changeset 5278 | a903b66822e2 |
parent 5220 | 07f80f447b27 |
child 5304 | c133f16febc7 |
--- a/src/HOL/simpdata.ML Thu Aug 06 15:47:26 1998 +0200 +++ b/src/HOL/simpdata.ML Thu Aug 06 15:48:13 1998 +0200 @@ -252,6 +252,9 @@ qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)" (K [rtac refl 1]); + +(** if-then-else rules **) + qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x" (K [Blast_tac 1]);