# HG changeset patch
# User ballarin
# Date 1472148521 -7200
# Node ID e7df93d4d9b84240af3d6fa64aca5199fb5b7eb5
# Parent  dacc380ab327b506d3ae313150dea53d24389983
Back to original example theorem.

diff -r dacc380ab327 -r e7df93d4d9b8 src/Doc/Locales/Examples.thy
--- a/src/Doc/Locales/Examples.thy	Thu Aug 25 20:08:40 2016 +0200
+++ b/src/Doc/Locales/Examples.thy	Thu Aug 25 20:08:41 2016 +0200
@@ -320,7 +320,8 @@
 
 text \<open>These assumptions refer to the predicates for infimum
   and supremum defined for @{text partial_order} in the previous
-  section.  We now introduce the notions of meet and join.\<close>
+  section.  We now introduce the notions of meet and join,
+  together with an example theorem.\<close>
 
   definition
     meet (infixl "\<sqinter>" 70) where "x \<sqinter> y = (THE inf. is_inf x y inf)"
@@ -345,8 +346,7 @@
       by (rule theI) (rule is_inf_uniq [OF _ \<open>is_inf x y i\<close>])
   qed
 
-  lemma %invisible meet_left [intro?]:
-    "x \<sqinter> y \<sqsubseteq> x"
+  lemma meet_left(*<*)[intro?](*>*): "x \<sqinter> y \<sqsubseteq> x"
     by (rule is_inf_lower) (rule is_inf_meet)
 
   lemma %invisible meet_right [intro?]:
@@ -568,8 +568,7 @@
 
 text \<open>Locales for total orders and distributive lattices follow to
   establish a sufficiently rich landscape of locales for
-  further examples in this tutorial.  Each comes with an example
-  theorem.\<close>
+  further examples in this tutorial.\<close>
 
   locale total_order = partial_order +
     assumes total: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
diff -r dacc380ab327 -r e7df93d4d9b8 src/Doc/Locales/Examples3.thy
--- 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}: \\