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