# HG changeset patch
# User ballarin
# Date 1367092605 -7200
# Node ID 8fcf6e32544e1e2ce7f3297f8fade55d55a3c440
# Parent  ad3a241def734cb002ce62b7cd0830f55b03884c
Clarified confusing sentence in locales tutorial.

diff -r ad3a241def73 -r 8fcf6e32544e src/Doc/Locales/Examples.thy
--- a/src/Doc/Locales/Examples.thy	Sat Apr 27 20:50:20 2013 +0200
+++ b/src/Doc/Locales/Examples.thy	Sat Apr 27 21:56:45 2013 +0200
@@ -86,10 +86,11 @@
     trans [trans] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?z\(\isasymrbrakk\) \(\Longrightarrow\) ?x \(\sqsubseteq\) ?z`
 \end{alltt}
 \end{small}
-  The keyword \isakeyword{notes} denotes a conclusion element.  There
-  is one conclusion, which was added automatically.  Instead, there is
-  only one assumption, namely @{term "partial_order le"}.  The locale
-  declaration has introduced the predicate @{term
+
+  This differs from the declaration.  The assumptions have turned into
+  conclusions, denoted by the keyword \isakeyword{notes}.  Also,
+  there is only one assumption, namely @{term "partial_order le"}.
+  The locale declaration has introduced the predicate @{term
   partial_order} to the theory.  This predicate is the
   \emph{locale predicate}.  Its definition may be inspected by
   issuing \isakeyword{thm} @{thm [source] partial_order_def}.