--- a/doc-src/Locales/Locales/Examples.thy Tue Dec 30 16:50:46 2008 +0100
+++ b/doc-src/Locales/Locales/Examples.thy Mon Jan 19 20:37:08 2009 +0100
@@ -608,9 +608,9 @@
and @{text lattice} be placed between @{text partial_order}
and @{text total_order}, as shown in Figure~\ref{fig:lattices}(b).
Changes to the locale hierarchy may be declared
- with the \isakeyword{interpretation} command. *}
+ with the \isakeyword{sublocale} command. *}
- interpretation %visible total_order \<subseteq> lattice
+ sublocale %visible total_order \<subseteq> lattice
txt {* This enters the context of locale @{text total_order}, in
which the goal @{subgoals [display]} must be shown. First, the
@@ -652,7 +652,7 @@
text {* Similarly, total orders are distributive lattices. *}
- interpretation total_order \<subseteq> distrib_lattice
+ sublocale total_order \<subseteq> distrib_lattice
proof unfold_locales
fix %"proof" x y z
show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")