# HG changeset patch
# User wenzelm
# Date 1185649754 -7200
# Node ID 8a4d5312d378b684c4e7b63c4a33e78b65496cdb
# Parent  77e3e5781a996bd6c4cf94fcbbd50db4d5c5ec0a
commands 'declare', 'declaration';

diff -r 77e3e5781a99 -r 8a4d5312d378 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sat Jul 28 20:40:31 2007 +0200
+++ b/doc-src/IsarRef/generic.tex	Sat Jul 28 21:09:14 2007 +0200
@@ -98,6 +98,48 @@
 \S\ref{sec:target}).
 
 
+\subsection{Generic declarations}
+
+Arbitrary operations on the background context may be wrapped-up as
+generic declaration elements.  Since the underlying concept of local
+theories may be subject to later re-interpretation, there is an
+additional dependency on a morphism that tells the difference of the
+original declaration context wrt.\ the application context encountered
+later on.  A fact declaration is an important special case: it
+consists of a theorem which is applied to the context by means of an
+attribute.
+
+\indexisarcmd{declaration}\indexisarcmd{declare}
+\begin{matharray}{rcl}
+  \isarcmd{declaration} & : & \isarkeep{local{\dsh}theory} \\
+  \isarcmd{declare} & : & \isarkeep{local{\dsh}theory} \\
+\end{matharray}
+
+\begin{rail}
+  'declaration' target? text
+  ;
+  'declare' target? (thmrefs + 'and')
+  ;
+\end{rail}
+
+\begin{descr}
+
+\item [$\isarkeyword{declaration}~d$] adds the declaration function
+  $d$ of ML type \verb,declaration, to the current local theory under
+  construction.  In later application contexts, the function is
+  transformed according to the morphisms being involved in the
+  interpretation hierarchy.
+
+\item [$\isarkeyword{declare}~thms$] declares theorems to the current
+  local 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.
+
+\end{descr}
+
+
 \subsection{Local theory targets}\label{sec:target}
 
 A local theory target is a context managed separately within the
diff -r 77e3e5781a99 -r 8a4d5312d378 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sat Jul 28 20:40:31 2007 +0200
+++ b/doc-src/IsarRef/pure.tex	Sat Jul 28 21:09:14 2007 +0200
@@ -1327,7 +1327,6 @@
 
 \indexisarcmd{apply}\indexisarcmd{apply-end}\indexisarcmd{done}
 \indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back}
-\indexisarcmd{declare}
 \begin{matharray}{rcl}
   \isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
   \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\
@@ -1335,21 +1334,15 @@
   \isarcmd{defer}^* & : & \isartrans{proof}{proof} \\
   \isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\
   \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
-  \isarcmd{declare}^* & : & \isarkeep{local{\dsh}theory} \\
 \end{matharray}
 
-\railalias{applyend}{apply\_end}
-\railterm{applyend}
-
 \begin{rail}
-  ( 'apply' | applyend ) method
+  ( 'apply' | 'apply\_end' ) method
   ;
   'defer' nat?
   ;
   'prefer' nat
   ;
-  'declare' target? (thmrefs + 'and')
-  ;
 \end{rail}
 
 \begin{descr}
@@ -1383,14 +1376,6 @@
   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 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}
 
 Any proper Isar proof method may be used with tactic script commands such as