src/HOL/Library/While_Combinator.thy

--- a/src/HOL/Library/While_Combinator.thy	Thu May 03 18:22:36 2001 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Fri May 04 15:38:48 2001 +0200
@@ -46,8 +46,8 @@
       then arbitrary
       else if b s then while_aux (b, c, c s)
       else s)"
+thm while_aux.simps
   apply (rule while_aux_tc [THEN while_aux.simps [THEN trans]])
-   apply (simp add: same_fst_def)
   apply (rule refl)
   done