--- 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
--- 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