--- a/src/HOL/ex/Tarski.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/ex/Tarski.thy Thu Feb 15 12:11:00 2018 +0100
@@ -385,7 +385,7 @@
by (simp add: isLub_def A_def r_def)
lemma isLubI:
- "\<lbrakk>L \<in> A; \<forall>y \<in> S. (y, L) \<in> r; (\<forall>z \<in> A. (\<forall>y \<in> S. (y, z):r) \<longrightarrow> (L, z) \<in> r)\<rbrakk> \<Longrightarrow> isLub S cl L"
+ "\<lbrakk>L \<in> A; \<forall>y \<in> S. (y, L) \<in> r; (\<forall>z \<in> A. (\<forall>y \<in> S. (y, z)\<in>r) \<longrightarrow> (L, z) \<in> r)\<rbrakk> \<Longrightarrow> isLub S cl L"
by (simp add: isLub_def A_def r_def)
end