--- a/src/HOL/Bali/AxSem.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Bali/AxSem.thy Thu Feb 15 12:11:00 2018 +0100
@@ -687,7 +687,7 @@
done
lemma weaken:
- "G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
+ "G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> \<forall>ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
apply (erule ax_derivs.induct)
(*42 subgoals*)
apply (tactic "ALLGOALS (strip_tac @{context})")