# HG changeset patch
# User blanchet
# Date 1467734421 -7200
# Node ID 786074d8d61bd13eedaedad7b0c782a1641cafc2
# Parent  6840e808fe4403c2255a83668185e4b1c0938d01
avoid reference to invisible theorem, by using another one instead (suggested by Anders Schlichtkrull; the document's author is incomunicado)

diff -r 6840e808fe44 -r 786074d8d61b src/Doc/Locales/Examples3.thy
--- 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}: \\