--- a/doc-src/IsarRef/Thy/document/Generic.tex Thu Mar 12 00:02:03 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Thu Mar 12 00:02:30 2009 +0100
@@ -160,8 +160,8 @@
compose rules by resolution. \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} resolves with the
first premise of \isa{a} (an alternative position may be also
specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic
- lifting process that is normally intended (cf.\ \verb|op RS| and \verb|op COMP| in
- \cite{isabelle-implementation}).
+ lifting process that is normally intended (cf.\ \verb|op RS| and
+ \verb|op COMP| in \cite{isabelle-implementation}).
\item \hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and \hyperlink{attribute.folded}{\mbox{\isa{folded}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} expand and fold back again the given
definitions throughout a rule.
--- a/doc-src/IsarRef/Thy/document/Proof.tex Thu Mar 12 00:02:03 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Thu Mar 12 00:02:30 2009 +0100
@@ -774,11 +774,11 @@
\item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,
elimination, or destruct rules.
- \item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} applies some theorem to all
- of the given rules \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} (in parallel). This
- corresponds to the \verb|op MRS| operation in ML,
- but note the reversed order. Positions may be effectively skipped
- by including ``\isa{{\isacharunderscore}}'' (underscore) as argument.
+ \item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} applies some
+ theorem to all of the given rules \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}}
+ (in parallel). This corresponds to the \verb|op MRS| operation in
+ ML, but note the reversed order. Positions may be effectively
+ skipped by including ``\isa{{\isacharunderscore}}'' (underscore) as argument.
\item \hyperlink{attribute.of}{\mbox{\isa{of}}}~\isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}} performs positional
instantiation of term variables. The terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}} are
@@ -890,10 +890,11 @@
\begin{description}
\item \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
- defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|Args.src -> Proof.context -> Proof.method|. Parsing concrete
- method syntax from \verb|Args.src| input can be quite tedious in
- general. The following simple examples are for methods without any
- explicit arguments, or a list of theorems, respectively.
+ defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|Args.src ->|\isasep\isanewline%
+\verb| Proof.context -> Proof.method|. Parsing concrete method syntax
+ from \verb|Args.src| input can be quite tedious in general. The
+ following simple examples are for methods without any explicit
+ arguments, or a list of theorems, respectively.
%FIXME proper antiquotations
{\footnotesize
--- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Mar 12 00:02:03 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Mar 12 00:02:30 2009 +0100
@@ -807,6 +807,7 @@
\indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{}{command}{local\_setup}\hypertarget{command.local-setup}{\hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
\end{matharray}
\begin{mldecls}
@@ -817,7 +818,7 @@
\begin{rail}
'use' name
;
- ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup') text
+ ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
;
\end{rail}
@@ -852,9 +853,14 @@
\item \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} changes the current theory
context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
- of type \verb|theory -> theory|. This enables
- to initialize any object-logic specific tools and packages written
- in ML, for example.
+ of type \verb|theory -> theory|. This enables to initialize
+ any object-logic specific tools and packages written in ML, for
+ example.
+
+ \item \hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}} is similar to \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} for
+ a local theory context, and an ML expression of type \verb|local_theory -> local_theory|. This allows to
+ invoke local theory specification packages without going through
+ concrete outer syntax, for example.
\item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
theorems produced in ML both in the theory context and the ML
--- a/etc/isar-keywords-ZF.el Thu Mar 12 00:02:03 2009 +0100
+++ b/etc/isar-keywords-ZF.el Thu Mar 12 00:02:30 2009 +0100
@@ -100,6 +100,7 @@
"let"
"linear_undo"
"local"
+ "local_setup"
"locale"
"method_setup"
"moreover"
@@ -379,6 +380,7 @@
"judgment"
"lemmas"
"local"
+ "local_setup"
"locale"
"method_setup"
"no_notation"
--- a/etc/isar-keywords.el Thu Mar 12 00:02:03 2009 +0100
+++ b/etc/isar-keywords.el Thu Mar 12 00:02:30 2009 +0100
@@ -127,6 +127,7 @@
"let"
"linear_undo"
"local"
+ "local_setup"
"locale"
"method_setup"
"moreover"
@@ -468,6 +469,7 @@
"judgment"
"lemmas"
"local"
+ "local_setup"
"locale"
"method_setup"
"no_notation"
--- a/lib/jedit/isabelle.xml Thu Mar 12 00:02:03 2009 +0100
+++ b/lib/jedit/isabelle.xml Thu Mar 12 00:02:30 2009 +0100
@@ -185,6 +185,7 @@
<OPERATOR>let</OPERATOR>
<INVALID>linear_undo</INVALID>
<OPERATOR>local</OPERATOR>
+ <OPERATOR>local_setup</OPERATOR>
<OPERATOR>locale</OPERATOR>
<OPERATOR>method_setup</OPERATOR>
<KEYWORD4>module_name</KEYWORD4>