updated generated files;
authorwenzelm
Thu Mar 12 00:02:30 2009 +0100 (2009-03-12)
changeset 30463f1cb00030d4f
parent 30462 0b857a58b15e
child 30464 a858ff86883b
child 30474 52e92009aacb
child 30476 0a41b0662264
updated generated files;
doc-src/IsarRef/Thy/document/Generic.tex
doc-src/IsarRef/Thy/document/Proof.tex
doc-src/IsarRef/Thy/document/Spec.tex
etc/isar-keywords-ZF.el
etc/isar-keywords.el
lib/jedit/isabelle.xml
     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>