doc-src/Locales/Locales/Examples.thy

 
   This style of working is illustrated in the block below, where
   notions of infimum and supremum for partial orders are introduced,
   together with theorems about their uniqueness.  *}
 
-  context partial_order begin
+  context partial_order
+  begin
 
   definition
     is_inf where "is_inf x y i =
       (i \<sqsubseteq> x \<and> i \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> i))"