# HG changeset patch
# User wenzelm
# Date 1163257901 -3600
# Node ID 01968a3365338835b84530c18b75097dd2cb2bdc
# Parent  fa16e4bf8717154b301724eb207835280bff9597
updated local theory targets;
removed 'context' as theory switch;

diff -r fa16e4bf8717 -r 01968a336533 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sat Nov 11 16:11:40 2006 +0100
+++ b/doc-src/IsarRef/pure.tex	Sat Nov 11 16:11:41 2006 +0100
@@ -24,11 +24,10 @@
 
 \subsection{Defining theories}\label{sec:begin-thy}
 
-\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{context}\indexisarcmd{end}
+\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}
 \begin{matharray}{rcl}
   \isarcmd{header} & : & \isarkeep{toplevel} \\
   \isarcmd{theory} & : & \isartrans{toplevel}{theory} \\
-  \isarcmd{context}^* & : & \isartrans{toplevel}{theory} \\
   \isarcmd{end} & : & \isartrans{theory}{toplevel} \\
 \end{matharray}
 
@@ -38,22 +37,20 @@
 proof as well.  In contrast, ``old-style'' Isabelle theories support batch
 processing only, with the proof scripts collected in separate ML files.
 
-The first ``real'' command of any theory has to be $\THEORY$, which starts a
-new theory based on the merge of existing ones.  Just preceding $\THEORY$,
-there may be an optional $\isarkeyword{header}$ declaration, which is relevant
-to document preparation only; it acts very much like a special pre-theory
-markup command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}).  The
-$\END$ command concludes a theory development; it has to be the very last
-command of any theory file loaded in batch-mode.  The theory context may be
-also changed interactively by $\CONTEXT$ without creating a new theory.
+The first ``real'' command of any theory has to be $\THEORY$, which
+starts a new theory based on the merge of existing ones.  Just
+preceding $\THEORY$, there may be an optional $\isarkeyword{header}$
+declaration, which is relevant to document preparation only; it acts
+very much like a special pre-theory markup command (cf.\ 
+\S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}).  The $\END$
+command concludes a theory development; it has to be the very last
+command of any theory file loaded in batch-mode.
 
 \begin{rail}
   'header' text
   ;
   'theory' name 'imports' (name +) uses? 'begin'
   ;
-  'context' name
-  ;
 
   uses: 'uses' ((name | parname) +);
 \end{rail}
@@ -86,14 +83,6 @@
   \emph{finished} theory $A$.  That file should not be included in the
   $\isarkeyword{files}$ dependency declaration, though.
   
-\item [$\CONTEXT~B$] enters an existing theory context, basically in read-only
-  mode, so only a limited set of commands may be performed without destroying
-  the theory.  Just as for $\THEORY$, the theory loader ensures that $B$ is
-  loaded and up-to-date.
-  
-  This command is occasionally useful for quick interactive experiments;
-  normally one should always commence a new context via $\THEORY$.
-  
 \item [$\END$] concludes the current theory definition or context switch.
   Note that this command cannot be undone, but the whole theory definition has
   to be retracted.
@@ -120,7 +109,7 @@
 tools).
 
 \begin{rail}
-  ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') locale? text
+  ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
   ;
   'text\_raw' text
   ;
@@ -138,8 +127,8 @@
 
 The $text$ argument of these markup commands (except for
 $\isarkeyword{text_raw}$) may contain references to formal entities
-(``antiquotations'', see also \S\ref{sec:antiq}).  These are interpreted in
-the present theory context, or the specified $locale$.
+(``antiquotations'', see also \S\ref{sec:antiq}).  These are
+interpreted in the present theory context, or the specified $target$.
 
 Any of these markup elements corresponds to a {\LaTeX} command with the name
 prefixed by \verb,\isamarkup,.  For the sectioning commands this is a plain
@@ -402,14 +391,14 @@
 \indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems}
 \begin{matharray}{rcll}
   \isarcmd{axioms} & : & \isartrans{theory}{theory} & (axiomatic!) \\
-  \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
-  \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
+  \isarcmd{lemmas} & : & \isarkeep{local{\dsh}theory} \\
+  \isarcmd{theorems} & : & isarkeep{local{\dsh}theory} \\
 \end{matharray}
 
 \begin{rail}
   'axioms' (axmdecl prop +)
   ;
-  ('lemmas' | 'theorems') locale? (thmdef? thmrefs + 'and')
+  ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
   ;
 \end{rail}
 
@@ -423,10 +412,10 @@
   Everyday work is typically done the hard way, with proper definitions and
   proven theorems.
   
-\item [$\isarkeyword{lemmas}~a = \vec b$] retrieves 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{lemmas}~a = \vec b$] retrieves and stores
+  existing facts in the theory context, or the specified target
+  context (see also \S\ref{sec:target}).  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.
@@ -876,9 +865,9 @@
 \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
 \indexisarcmd{print-statement}
 \begin{matharray}{rcl}
-  \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
-  \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
-  \isarcmd{corollary} & : & \isartrans{theory}{proof(prove)} \\
+  \isarcmd{lemma} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+  \isarcmd{theorem} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+  \isarcmd{corollary} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
   \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
   \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
   \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
@@ -914,7 +903,7 @@
 and assumptions, cf.\ \S\ref{sec:obtain}).
 
 \begin{rail}
-  ('lemma' | 'theorem' | 'corollary') locale? (goal | longgoal)
+  ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
   ;
   ('have' | 'show' | 'hence' | 'thus') goal
   ;
@@ -1345,7 +1334,7 @@
   \isarcmd{defer}^* & : & \isartrans{proof}{proof} \\
   \isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\
   \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
-  \isarcmd{declare}^* & : & \isartrans{theory}{theory} \\
+  \isarcmd{declare}^* & : & \isarkeep{local{\dsh}theory} \\
 \end{matharray}
 
 \railalias{applyend}{apply\_end}
@@ -1358,7 +1347,7 @@
   ;
   'prefer' nat
   ;
-  'declare' locale? (thmrefs + 'and')
+  'declare' target? (thmrefs + 'and')
   ;
 \end{rail}
 
@@ -1393,12 +1382,13 @@
   the latest proof command.  Basically, any proof command may return multiple
   results.
   
-\item [$\isarkeyword{declare}~thms$] declares theorems to the current theory
-  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.
+\item [$\isarkeyword{declare}~thms$] declares theorems to the current
+  theory context (or the specified target context, see also
+  \S\ref{sec:target}).  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}