src/HOL/Library/While_Combinator.thy
changeset 61424 c3658c18b7bc
parent 61166 5976fe402824
child 63040 eb4ddd18d635
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -349,7 +349,7 @@
     1.4      by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
     1.5    { assume "ws = []"
     1.6      hence ?thesis using I
     1.7 -      by (auto simp del:Image_Collect_split dest: Image_closed_trancl)
     1.8 +      by (auto simp del:Image_Collect_case_prod dest: Image_closed_trancl)
     1.9    } moreover
    1.10    { assume "ws \<noteq> []"
    1.11      hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]