--- a/src/HOL/Bali/AxSound.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Bali/AxSound.thy Thu Feb 15 12:11:00 2018 +0100
@@ -300,7 +300,7 @@
cases. Auto will then solve premise 6 and 7.
*)
-lemma all_empty: "(!x. P) = P"
+lemma all_empty: "(\<forall>x. P) = P"
by simp
corollary evaln_type_sound: