--- a/src/HOL/ex/Tarski.thy Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/ex/Tarski.thy Wed Nov 04 08:13:49 2015 +0100
@@ -119,7 +119,7 @@
locale CL = S +
assumes cl_co: "cl : CompleteLattice"
-sublocale CL < po: PO
+sublocale CL < po?: PO
apply (simp_all add: A_def r_def)
apply unfold_locales
using cl_co unfolding CompleteLattice_def by auto
@@ -130,7 +130,7 @@
assumes f_cl: "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
defines P_def: "P == fix f A"
-sublocale CLF < cl: CL
+sublocale CLF < cl?: CL
apply (simp_all add: A_def r_def)
apply unfold_locales
using f_cl unfolding CLF_set_def by auto