--- a/src/HOL/Library/While_Combinator.thy Fri Feb 23 21:46:30 2018 +0100
+++ b/src/HOL/Library/While_Combinator.thy Sat Feb 24 17:21:35 2018 +0100
@@ -68,7 +68,7 @@
define k where "k = (LEAST k. \<not> b ((c ^^ k) s))"
from assms have t: "t = (c ^^ k) s"
by (simp add: while_option_def k_def split: if_splits)
- have 1: "ALL i<k. b ((c ^^ i) s)"
+ have 1: "\<forall>i<k. b ((c ^^ i) s)"
by (auto simp: k_def dest: not_less_Least)
{ fix i assume "i \<le> k" then have "P ((c ^^ i) s)"
--- a/src/HOL/List.thy Fri Feb 23 21:46:30 2018 +0100
+++ b/src/HOL/List.thy Sat Feb 24 17:21:35 2018 +0100
@@ -1716,7 +1716,7 @@
lemma list_eq_iff_nth_eq:
- "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
+ "(xs = ys) = (length xs = length ys \<and> (\<forall>i<length xs. xs!i = ys!i))"
apply(induct xs arbitrary: ys)
apply force
apply(case_tac ys)
@@ -1772,7 +1772,7 @@
by (auto simp add: set_conv_nth)
lemma all_nth_imp_all_set:
- "\<lbrakk>!i < length xs. P(xs!i); x \<in> set xs\<rbrakk> \<Longrightarrow> P x"
+ "\<lbrakk>\<forall>i < length xs. P(xs!i); x \<in> set xs\<rbrakk> \<Longrightarrow> P x"
by (auto simp add: set_conv_nth)
lemma all_set_conv_all_nth:
@@ -3150,7 +3150,7 @@
done
lemma nth_equalityI:
- "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
+ "[| length xs = length ys; \<forall>i < length xs. xs!i = ys!i |] ==> xs = ys"
by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
lemma map_nth:
--- a/src/HOL/MicroJava/DFA/Typing_Framework.thy Fri Feb 23 21:46:30 2018 +0100
+++ b/src/HOL/MicroJava/DFA/Typing_Framework.thy Sat Feb 24 17:21:35 2018 +0100
@@ -18,12 +18,12 @@
"stable r step ss p == \<forall>(q,s')\<in>set(step p (ss!p)). s' <=_r ss!q"
definition stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool" where
-"stables r step ss == !p<size ss. stable r step ss p"
+"stables r step ss == \<forall>p<size ss. stable r step ss p"
definition wt_step ::
"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool" where
"wt_step r T step ts ==
- !p<size(ts). ts!p ~= T & stable r step ts p"
+ \<forall>p<size(ts). ts!p ~= T & stable r step ts p"
definition is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type
\<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool" where
--- a/src/HOL/UNITY/Comp/Alloc.thy Fri Feb 23 21:46:30 2018 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Sat Feb 24 17:21:35 2018 +0100
@@ -943,7 +943,7 @@
done
text\<open>progress (2), step 4\<close>
-lemma System_Bounded_allocAsk: "System \<in> Always {s. ALL i<Nclients.
+lemma System_Bounded_allocAsk: "System \<in> Always {s. \<forall>i<Nclients.
\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT}"
apply (auto simp add: Collect_all_imp_eq)
apply (tactic \<open>resolve_tac @{context} [Always_Int_rule [@{thm Always_allocAsk_le_ask},