--- a/src/Doc/Locales/Examples3.thy Thu Aug 25 20:08:40 2016 +0200
+++ b/src/Doc/Locales/Examples3.thy Thu Aug 25 20:08:41 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.ex_sup} from locale @{text lattice}: \\
- \quad @{thm int.ex_sup} \\
+ @{thm [source] int.meet_left} from locale @{text lattice}: \\
+ \quad @{thm int.meet_left} \\
@{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}: \\