diff -r e4297d03e5d2 -r a903b66822e2 src/HOL/simpdata.ML
--- 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]);