# HG changeset patch
# User wenzelm
# Date 1519489295 -3600
# Node ID 5a1b299fe4af77c7ceabf068df0eff2ddcfa94e4
# Parent  3f611f444c2da26486d7e735e185afc93dc312dd
more symbols;

diff -r 3f611f444c2d -r 5a1b299fe4af src/HOL/Library/While_Combinator.thy
--- 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)"
diff -r 3f611f444c2d -r 5a1b299fe4af src/HOL/List.thy
--- 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:
diff -r 3f611f444c2d -r 5a1b299fe4af src/HOL/MicroJava/DFA/Typing_Framework.thy
--- 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
diff -r 3f611f444c2d -r 5a1b299fe4af src/HOL/UNITY/Comp/Alloc.thy
--- 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},