src/HOL/Library/While_Combinator.thy
changeset 67717 5a1b299fe4af
parent 67613 ce654b0e6d69
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Feb 23 21:46:30 2018 +0100
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Sat Feb 24 17:21:35 2018 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4    define k where "k = (LEAST k. \<not> b ((c ^^ k) s))"
     1.5    from assms have t: "t = (c ^^ k) s"
     1.6      by (simp add: while_option_def k_def split: if_splits)    
     1.7 -  have 1: "ALL i<k. b ((c ^^ i) s)"
     1.8 +  have 1: "\<forall>i<k. b ((c ^^ i) s)"
     1.9      by (auto simp: k_def dest: not_less_Least)
    1.10  
    1.11    { fix i assume "i \<le> k" then have "P ((c ^^ i) s)"