1.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex Thu Mar 12 00:02:03 2009 +0100
1.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Thu Mar 12 00:02:30 2009 +0100
1.3 @@ -160,8 +160,8 @@
1.4 compose rules by resolution. \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} resolves with the
1.5 first premise of \isa{a} (an alternative position may be also
1.6 specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic
1.7 - lifting process that is normally intended (cf.\ \verb|op RS| and \verb|op COMP| in
1.8 - \cite{isabelle-implementation}).
1.9 + lifting process that is normally intended (cf.\ \verb|op RS| and
1.10 + \verb|op COMP| in \cite{isabelle-implementation}).
1.11
1.12 \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
1.13 definitions throughout a rule.
2.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex Thu Mar 12 00:02:03 2009 +0100
2.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Thu Mar 12 00:02:30 2009 +0100
2.3 @@ -774,11 +774,11 @@
2.4 \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,
2.5 elimination, or destruct rules.
2.6
2.7 - \item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} applies some theorem to all
2.8 - of the given rules \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} (in parallel). This
2.9 - corresponds to the \verb|op MRS| operation in ML,
2.10 - but note the reversed order. Positions may be effectively skipped
2.11 - by including ``\isa{{\isacharunderscore}}'' (underscore) as argument.
2.12 + \item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} applies some
2.13 + theorem to all of the given rules \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}}
2.14 + (in parallel). This corresponds to the \verb|op MRS| operation in
2.15 + ML, but note the reversed order. Positions may be effectively
2.16 + skipped by including ``\isa{{\isacharunderscore}}'' (underscore) as argument.
2.17
2.18 \item \hyperlink{attribute.of}{\mbox{\isa{of}}}~\isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}} performs positional
2.19 instantiation of term variables. The terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}} are
2.20 @@ -890,10 +890,11 @@
2.21 \begin{description}
2.22
2.23 \item \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
2.24 - 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
2.25 - method syntax from \verb|Args.src| input can be quite tedious in
2.26 - general. The following simple examples are for methods without any
2.27 - explicit arguments, or a list of theorems, respectively.
2.28 + 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%
2.29 +\verb| Proof.context -> Proof.method|. Parsing concrete method syntax
2.30 + from \verb|Args.src| input can be quite tedious in general. The
2.31 + following simple examples are for methods without any explicit
2.32 + arguments, or a list of theorems, respectively.
2.33
2.34 %FIXME proper antiquotations
2.35 {\footnotesize
3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Mar 12 00:02:03 2009 +0100
3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Mar 12 00:02:30 2009 +0100
3.3 @@ -807,6 +807,7 @@
3.4 \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
3.5 \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
3.6 \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
3.7 + \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}} \\
3.8 \end{matharray}
3.9
3.10 \begin{mldecls}
3.11 @@ -817,7 +818,7 @@
3.12 \begin{rail}
3.13 'use' name
3.14 ;
3.15 - ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup') text
3.16 + ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
3.17 ;
3.18 \end{rail}
3.19
3.20 @@ -852,9 +853,14 @@
3.21
3.22 \item \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} changes the current theory
3.23 context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
3.24 - of type \verb|theory -> theory|. This enables
3.25 - to initialize any object-logic specific tools and packages written
3.26 - in ML, for example.
3.27 + of type \verb|theory -> theory|. This enables to initialize
3.28 + any object-logic specific tools and packages written in ML, for
3.29 + example.
3.30 +
3.31 + \item \hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}} is similar to \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} for
3.32 + a local theory context, and an ML expression of type \verb|local_theory -> local_theory|. This allows to
3.33 + invoke local theory specification packages without going through
3.34 + concrete outer syntax, for example.
3.35
3.36 \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
3.37 theorems produced in ML both in the theory context and the ML
4.1 --- a/etc/isar-keywords-ZF.el Thu Mar 12 00:02:03 2009 +0100
4.2 +++ b/etc/isar-keywords-ZF.el Thu Mar 12 00:02:30 2009 +0100
4.3 @@ -100,6 +100,7 @@
4.4 "let"
4.5 "linear_undo"
4.6 "local"
4.7 + "local_setup"
4.8 "locale"
4.9 "method_setup"
4.10 "moreover"
4.11 @@ -379,6 +380,7 @@
4.12 "judgment"
4.13 "lemmas"
4.14 "local"
4.15 + "local_setup"
4.16 "locale"
4.17 "method_setup"
4.18 "no_notation"
5.1 --- a/etc/isar-keywords.el Thu Mar 12 00:02:03 2009 +0100
5.2 +++ b/etc/isar-keywords.el Thu Mar 12 00:02:30 2009 +0100
5.3 @@ -127,6 +127,7 @@
5.4 "let"
5.5 "linear_undo"
5.6 "local"
5.7 + "local_setup"
5.8 "locale"
5.9 "method_setup"
5.10 "moreover"
5.11 @@ -468,6 +469,7 @@
5.12 "judgment"
5.13 "lemmas"
5.14 "local"
5.15 + "local_setup"
5.16 "locale"
5.17 "method_setup"
5.18 "no_notation"
6.1 --- a/lib/jedit/isabelle.xml Thu Mar 12 00:02:03 2009 +0100
6.2 +++ b/lib/jedit/isabelle.xml Thu Mar 12 00:02:30 2009 +0100
6.3 @@ -185,6 +185,7 @@
6.4 <OPERATOR>let</OPERATOR>
6.5 <INVALID>linear_undo</INVALID>
6.6 <OPERATOR>local</OPERATOR>
6.7 + <OPERATOR>local_setup</OPERATOR>
6.8 <OPERATOR>locale</OPERATOR>
6.9 <OPERATOR>method_setup</OPERATOR>
6.10 <KEYWORD4>module_name</KEYWORD4>