avoid reference to invisible theorem, by using another one instead (suggested by Anders Schlichtkrull; the document's author is incomunicado)

--- a/src/Doc/Locales/Examples3.thy	Tue Jul 05 17:52:08 2016 +0200
+++ b/src/Doc/Locales/Examples3.thy	Tue Jul 05 18:00:21 2016 +0200
@@ -91,8 +91,8 @@
 \begin{tabular}{l}
   @{thm [source] int.less_def} from locale @{text partial_order}: \\
   \quad @{thm int.less_def} \\
-  @{thm [source] int.meet_left} from locale @{text lattice}: \\
-  \quad @{thm int.meet_left} \\
+  @{thm [source] int.ex_sup} from locale @{text lattice}: \\
+  \quad @{thm int.ex_sup} \\
   @{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\
   \quad @{thm int.join_distr} \\
   @{thm [source] int.less_total} from locale @{text total_order}: \\