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