doc-src/IsarRef/pure.tex

 \end{matharray}
 
 \begin{rail}
   'axioms' (axmdecl prop +)
   ;
-  ('lemmas' | 'theorems') (thmdef? thmrefs + 'and')
-  ;
-\end{rail}
-
-\begin{descr}
+  ('lemmas' | 'theorems') locale? (thmdef? thmrefs + 'and')
+  ;
+\end{rail}
+
+\begin{descr}
+  
 \item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as
   axioms of the meta-logic.  In fact, axioms are ``axiomatic theorems'', and
   may be referred later just as any other theorem.
   
   Axioms are usually only introduced when declaring new logical systems.
   Everyday work is typically done the hard way, with proper definitions and
   actual proven theorems.
-\item [$\isarkeyword{lemmas}~a = \vec b$] stores existing facts.  Typical
-  applications would also involve attributes, to declare Simplifier rules, for
-  example.
+  
+\item [$\isarkeyword{lemmas}~a = \vec b$] restrieves and stores existing facts
+  in the theory context, or the specified locale (see also
+  \S\ref{sec:locale}).  Typical applications would also involve attributes, to
+  declare Simplifier rules, for example.
+  
 \item [$\isarkeyword{theorems}$] is essentially the same as
   $\isarkeyword{lemmas}$, but marks the result as a different kind of facts.
+
 \end{descr}
 
 
 \subsection{Name spaces}
 

 Automated methods (such as $simp$ or $auto$) just insert any given facts
 before their usual operation.  Depending on the kind of procedure involved,
 the order of facts is less significant here.
 
 
-\subsection{Goal statements}
+\subsection{Goal statements}\label{sec:goals}
 
 \indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary}
 \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
 \begin{matharray}{rcl}
   \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\

   ;
   'defer' nat?
   ;
   'prefer' nat
   ;
-  'declare' thmrefs
+  'declare' locale? (thmrefs + 'and')
   ;
 \end{rail}
 
 \begin{descr}
 \item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike

   the latest proof command.\footnote{Unlike the ML function \texttt{back}
     \cite{isabelle-ref}, the Isar command does not search upwards for further
     branch points.} Basically, any proof command may return multiple results.
   
 \item [$\isarkeyword{declare}~thms$] declares theorems to the current theory
-  context.  No theorem binding is involved here, unlike
-  $\isarkeyword{theorems}$ or $\isarkeyword{lemmas}$ (cf.\ 
-  \S\ref{sec:axms-thms}).  So $\isarkeyword{declare}$ only has the effect of
-  applying attributes as included in the theorem specification.
+  context (or the specified locale, see also \S\ref{sec:locale}).  No theorem
+  binding is involved here, unlike $\isarkeyword{theorems}$ or
+  $\isarkeyword{lemmas}$ (cf.\ \S\ref{sec:axms-thms}), so
+  $\isarkeyword{declare}$ only has the effect of applying attributes as
+  included in the theorem specification.
 \end{descr}
 
 Any proper Isar proof method may be used with tactic script commands such as
 $\APPLYNAME$.  A few additional emulations of actual tactics are provided as
 well; these would be never used in actual structured proofs, of course.