updated generated file;
authorwenzelm
Mon Jun 02 23:12:23 2008 +0200 (2008-06-02)
changeset 270472dcdea037385
parent 27046 51c2635dd89c
child 27048 0e86aab627f3
updated generated file;
doc-src/IsarRef/Thy/document/Generic.tex
doc-src/IsarRef/Thy/document/HOL_Specific.tex
doc-src/IsarRef/Thy/document/Spec.tex
     1.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Mon Jun 02 23:12:09 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Mon Jun 02 23:12:23 2008 +0200
     1.3 @@ -173,8 +173,8 @@
     1.4    \item [\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}~\isa{n}] rotate the premises of a
     1.5    theorem by \isa{n} (default 1).
     1.6  
     1.7 -  \item [\hyperlink{attribute.Pure.elim-format}{\mbox{\isa{Pure{\isachardot}elim{\isacharunderscore}format}}}] turns a destruction rule into
     1.8 -  elimination rule format, by resolving with the rule \isa{{\isachardoublequote}PROP\ A\ {\isasymLongrightarrow}\ {\isacharparenleft}PROP\ A\ {\isasymLongrightarrow}\ PROP\ B{\isacharparenright}\ {\isasymLongrightarrow}\ PROP\ B{\isachardoublequote}}.
     1.9 +  \item [\hyperlink{attribute.Pure.elim-format}{\mbox{\isa{elim{\isacharunderscore}format}}}] turns a destruction rule
    1.10 +  into elimination rule format, by resolving with the rule \isa{{\isachardoublequote}PROP\ A\ {\isasymLongrightarrow}\ {\isacharparenleft}PROP\ A\ {\isasymLongrightarrow}\ PROP\ B{\isacharparenright}\ {\isasymLongrightarrow}\ PROP\ B{\isachardoublequote}}.
    1.11    
    1.12    Note that the Classical Reasoner (\secref{sec:classical}) provides
    1.13    its own version of this operation.
    1.14 @@ -191,6 +191,72 @@
    1.15  \end{isamarkuptext}%
    1.16  \isamarkuptrue%
    1.17  %
    1.18 +\isamarkupsubsection{Low-level equational reasoning%
    1.19 +}
    1.20 +\isamarkuptrue%
    1.21 +%
    1.22 +\begin{isamarkuptext}%
    1.23 +\begin{matharray}{rcl}
    1.24 +    \indexdef{}{method}{subst}\hypertarget{method.subst}{\hyperlink{method.subst}{\mbox{\isa{subst}}}} & : & \isarmeth \\
    1.25 +    \indexdef{}{method}{hypsubst}\hypertarget{method.hypsubst}{\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}} & : & \isarmeth \\
    1.26 +    \indexdef{}{method}{split}\hypertarget{method.split}{\hyperlink{method.split}{\mbox{\isa{split}}}} & : & \isarmeth \\
    1.27 +  \end{matharray}
    1.28 +
    1.29 +  \begin{rail}
    1.30 +    'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
    1.31 +    ;
    1.32 +    'split' ('(' 'asm' ')')? thmrefs
    1.33 +    ;
    1.34 +  \end{rail}
    1.35 +
    1.36 +  These methods provide low-level facilities for equational reasoning
    1.37 +  that are intended for specialized applications only.  Normally,
    1.38 +  single step calculations would be performed in a structured text
    1.39 +  (see also \secref{sec:calculation}), while the Simplifier methods
    1.40 +  provide the canonical way for automated normalization (see
    1.41 +  \secref{sec:simplifier}).
    1.42 +
    1.43 +  \begin{descr}
    1.44 +
    1.45 +  \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{eq}] performs a single substitution
    1.46 +  step using rule \isa{eq}, which may be either a meta or object
    1.47 +  equality.
    1.48 +
    1.49 +  \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ eq{\isachardoublequote}}] substitutes in an
    1.50 +  assumption.
    1.51 +
    1.52 +  \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs several
    1.53 +  substitutions in the conclusion. The numbers \isa{i} to \isa{j}
    1.54 +  indicate the positions to substitute at.  Positions are ordered from
    1.55 +  the top of the term tree moving down from left to right. For
    1.56 +  example, in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}} there are three positions
    1.57 +  where commutativity of \isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}} is applicable: 1 refers to the
    1.58 +  whole term, 2 to \isa{{\isachardoublequote}a\ {\isacharplus}\ b{\isachardoublequote}} and 3 to \isa{{\isachardoublequote}c\ {\isacharplus}\ d{\isachardoublequote}}.
    1.59 +
    1.60 +  If the positions in the list \isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}{\isachardoublequote}} are non-overlapping
    1.61 +  (e.g.\ \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}\ {\isadigit{3}}{\isacharparenright}{\isachardoublequote}} in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}}) you may
    1.62 +  assume all substitutions are performed simultaneously.  Otherwise
    1.63 +  the behaviour of \isa{subst} is not specified.
    1.64 +
    1.65 +  \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ {\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs the
    1.66 +  substitutions in the assumptions.  Positions \isa{{\isachardoublequote}{\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{1}}{\isachardoublequote}}
    1.67 +  refer to assumption 1, positions \isa{{\isachardoublequote}i\isactrlsub {\isadigit{1}}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{2}}{\isachardoublequote}}
    1.68 +  to assumption 2, and so on.
    1.69 +
    1.70 +  \item [\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}] performs substitution using some
    1.71 +  assumption; this only works for equations of the form \isa{{\isachardoublequote}x\ {\isacharequal}\ t{\isachardoublequote}} where \isa{x} is a free or bound variable.
    1.72 +
    1.73 +  \item [\hyperlink{method.split}{\mbox{\isa{split}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] performs
    1.74 +  single-step case splitting using the given rules.  By default,
    1.75 +  splitting is performed in the conclusion of a goal; the \isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}{\isachardoublequote}} option indicates to operate on assumptions instead.
    1.76 +  
    1.77 +  Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
    1.78 +  application of split rules as declared in the current context.
    1.79 +
    1.80 +  \end{descr}%
    1.81 +\end{isamarkuptext}%
    1.82 +\isamarkuptrue%
    1.83 +%
    1.84  \isamarkupsubsection{Further tactic emulations \label{sec:tactics}%
    1.85  }
    1.86  \isamarkuptrue%
    1.87 @@ -498,72 +564,6 @@
    1.88  \end{isamarkuptext}%
    1.89  \isamarkuptrue%
    1.90  %
    1.91 -\isamarkupsubsection{Low-level equational reasoning%
    1.92 -}
    1.93 -\isamarkuptrue%
    1.94 -%
    1.95 -\begin{isamarkuptext}%
    1.96 -\begin{matharray}{rcl}
    1.97 -    \indexdef{}{method}{subst}\hypertarget{method.subst}{\hyperlink{method.subst}{\mbox{\isa{subst}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    1.98 -    \indexdef{}{method}{hypsubst}\hypertarget{method.hypsubst}{\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    1.99 -    \indexdef{}{method}{split}\hypertarget{method.split}{\hyperlink{method.split}{\mbox{\isa{split}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
   1.100 -  \end{matharray}
   1.101 -
   1.102 -  \begin{rail}
   1.103 -    'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
   1.104 -    ;
   1.105 -    'split' ('(' 'asm' ')')? thmrefs
   1.106 -    ;
   1.107 -  \end{rail}
   1.108 -
   1.109 -  These methods provide low-level facilities for equational reasoning
   1.110 -  that are intended for specialized applications only.  Normally,
   1.111 -  single step calculations would be performed in a structured text
   1.112 -  (see also \secref{sec:calculation}), while the Simplifier methods
   1.113 -  provide the canonical way for automated normalization (see
   1.114 -  \secref{sec:simplifier}).
   1.115 -
   1.116 -  \begin{descr}
   1.117 -
   1.118 -  \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{eq}] performs a single substitution
   1.119 -  step using rule \isa{eq}, which may be either a meta or object
   1.120 -  equality.
   1.121 -
   1.122 -  \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ eq{\isachardoublequote}}] substitutes in an
   1.123 -  assumption.
   1.124 -
   1.125 -  \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs several
   1.126 -  substitutions in the conclusion. The numbers \isa{i} to \isa{j}
   1.127 -  indicate the positions to substitute at.  Positions are ordered from
   1.128 -  the top of the term tree moving down from left to right. For
   1.129 -  example, in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}} there are three positions
   1.130 -  where commutativity of \isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}} is applicable: 1 refers to the
   1.131 -  whole term, 2 to \isa{{\isachardoublequote}a\ {\isacharplus}\ b{\isachardoublequote}} and 3 to \isa{{\isachardoublequote}c\ {\isacharplus}\ d{\isachardoublequote}}.
   1.132 -
   1.133 -  If the positions in the list \isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}{\isachardoublequote}} are non-overlapping
   1.134 -  (e.g.\ \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}\ {\isadigit{3}}{\isacharparenright}{\isachardoublequote}} in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}}) you may
   1.135 -  assume all substitutions are performed simultaneously.  Otherwise
   1.136 -  the behaviour of \isa{subst} is not specified.
   1.137 -
   1.138 -  \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ {\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs the
   1.139 -  substitutions in the assumptions.  Positions \isa{{\isachardoublequote}{\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{1}}{\isachardoublequote}}
   1.140 -  refer to assumption 1, positions \isa{{\isachardoublequote}i\isactrlsub {\isadigit{1}}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{2}}{\isachardoublequote}}
   1.141 -  to assumption 2, and so on.
   1.142 -
   1.143 -  \item [\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}] performs substitution using some
   1.144 -  assumption; this only works for equations of the form \isa{{\isachardoublequote}x\ {\isacharequal}\ t{\isachardoublequote}} where \isa{x} is a free or bound variable.
   1.145 -
   1.146 -  \item [\hyperlink{method.split}{\mbox{\isa{split}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] performs
   1.147 -  single-step case splitting using the given rules.  By default,
   1.148 -  splitting is performed in the conclusion of a goal; the \isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}{\isachardoublequote}} option indicates to operate on assumptions instead.
   1.149 -  
   1.150 -  Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
   1.151 -  application of split rules as declared in the current context.
   1.152 -
   1.153 -  \end{descr}%
   1.154 -\end{isamarkuptext}%
   1.155 -\isamarkuptrue%
   1.156 -%
   1.157  \isamarkupsection{The Classical Reasoner \label{sec:classical}%
   1.158  }
   1.159  \isamarkuptrue%
   1.160 @@ -778,7 +778,7 @@
   1.161  \end{isamarkuptext}%
   1.162  \isamarkuptrue%
   1.163  %
   1.164 -\isamarkupsection{General logic setup \label{sec:object-logic}%
   1.165 +\isamarkupsection{Object-logic setup \label{sec:object-logic}%
   1.166  }
   1.167  \isamarkuptrue%
   1.168  %
     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jun 02 23:12:09 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jun 02 23:12:23 2008 +0200
     2.3 @@ -616,54 +616,6 @@
     2.4  \end{isamarkuptext}%
     2.5  \isamarkuptrue%
     2.6  %
     2.7 -\isamarkupsection{Definition by specification \label{sec:hol-specification}%
     2.8 -}
     2.9 -\isamarkuptrue%
    2.10 -%
    2.11 -\begin{isamarkuptext}%
    2.12 -\begin{matharray}{rcl}
    2.13 -    \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
    2.14 -    \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
    2.15 -  \end{matharray}
    2.16 -
    2.17 -  \begin{rail}
    2.18 -  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
    2.19 -  ;
    2.20 -  decl: ((name ':')? term '(' 'overloaded' ')'?)
    2.21 -  \end{rail}
    2.22 -
    2.23 -  \begin{descr}
    2.24 -
    2.25 -  \item [\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a
    2.26 -  goal stating the existence of terms with the properties specified to
    2.27 -  hold for the constants given in \isa{decls}.  After finishing the
    2.28 -  proof, the theory will be augmented with definitions for the given
    2.29 -  constants, as well as with theorems stating the properties for these
    2.30 -  constants.
    2.31 -
    2.32 -  \item [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
    2.33 -  up a goal stating the existence of terms with the properties
    2.34 -  specified to hold for the constants given in \isa{decls}.  After
    2.35 -  finishing the proof, the theory will be augmented with axioms
    2.36 -  expressing the properties given in the first place.
    2.37 -
    2.38 -  \item [\isa{decl}] declares a constant to be defined by the
    2.39 -  specification given.  The definition for the constant \isa{c} is
    2.40 -  bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
    2.41 -  the declaration.  Overloaded constants should be declared as such.
    2.42 -
    2.43 -  \end{descr}
    2.44 -
    2.45 -  Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} is to some extent a matter of style.  \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by
    2.46 -  construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
    2.47 -  user has explicitly proven it to be safe.  A practical issue must be
    2.48 -  considered, though: After introducing two constants with the same
    2.49 -  properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
    2.50 -  that the two constants are, in fact, equal.  If this might be a
    2.51 -  problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
    2.52 -\end{isamarkuptext}%
    2.53 -\isamarkuptrue%
    2.54 -%
    2.55  \isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
    2.56  }
    2.57  \isamarkuptrue%
    2.58 @@ -1140,6 +1092,54 @@
    2.59  \end{isamarkuptext}%
    2.60  \isamarkuptrue%
    2.61  %
    2.62 +\isamarkupsection{Definition by specification \label{sec:hol-specification}%
    2.63 +}
    2.64 +\isamarkuptrue%
    2.65 +%
    2.66 +\begin{isamarkuptext}%
    2.67 +\begin{matharray}{rcl}
    2.68 +    \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
    2.69 +    \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
    2.70 +  \end{matharray}
    2.71 +
    2.72 +  \begin{rail}
    2.73 +  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
    2.74 +  ;
    2.75 +  decl: ((name ':')? term '(' 'overloaded' ')'?)
    2.76 +  \end{rail}
    2.77 +
    2.78 +  \begin{descr}
    2.79 +
    2.80 +  \item [\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a
    2.81 +  goal stating the existence of terms with the properties specified to
    2.82 +  hold for the constants given in \isa{decls}.  After finishing the
    2.83 +  proof, the theory will be augmented with definitions for the given
    2.84 +  constants, as well as with theorems stating the properties for these
    2.85 +  constants.
    2.86 +
    2.87 +  \item [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
    2.88 +  up a goal stating the existence of terms with the properties
    2.89 +  specified to hold for the constants given in \isa{decls}.  After
    2.90 +  finishing the proof, the theory will be augmented with axioms
    2.91 +  expressing the properties given in the first place.
    2.92 +
    2.93 +  \item [\isa{decl}] declares a constant to be defined by the
    2.94 +  specification given.  The definition for the constant \isa{c} is
    2.95 +  bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
    2.96 +  the declaration.  Overloaded constants should be declared as such.
    2.97 +
    2.98 +  \end{descr}
    2.99 +
   2.100 +  Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} is to some extent a matter of style.  \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by
   2.101 +  construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
   2.102 +  user has explicitly proven it to be safe.  A practical issue must be
   2.103 +  considered, though: After introducing two constants with the same
   2.104 +  properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
   2.105 +  that the two constants are, in fact, equal.  If this might be a
   2.106 +  problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
   2.107 +\end{isamarkuptext}%
   2.108 +\isamarkuptrue%
   2.109 +%
   2.110  \isadelimtheory
   2.111  %
   2.112  \endisadelimtheory
     3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Jun 02 23:12:09 2008 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Jun 02 23:12:23 2008 +0200
     3.3 @@ -20,7 +20,7 @@
     3.4  %
     3.5  \endisadelimtheory
     3.6  %
     3.7 -\isamarkupchapter{Specifications%
     3.8 +\isamarkupchapter{Theory specifications%
     3.9  }
    3.10  \isamarkuptrue%
    3.11  %
    3.12 @@ -1100,7 +1100,7 @@
    3.13  \begin{matharray}{rcll}
    3.14      \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
    3.15      \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isarkeep{local{\dsh}theory} \\
    3.16 -    \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & isarkeep{local{\dsh}theory} \\
    3.17 +    \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isarkeep{local{\dsh}theory} \\
    3.18    \end{matharray}
    3.19  
    3.20    \begin{rail}
    3.21 @@ -1319,15 +1319,15 @@
    3.22  %FIXME proper antiquotations
    3.23  \begin{ttbox}
    3.24  val parse_ast_translation:
    3.25 -  (string * (Context.generic -> ast list -> ast)) list
    3.26 +  (string * (Proof.context -> ast list -> ast)) list
    3.27  val parse_translation:
    3.28 -  (string * (Context.generic -> term list -> term)) list
    3.29 +  (string * (Proof.context -> term list -> term)) list
    3.30  val print_translation:
    3.31 -  (string * (Context.generic -> term list -> term)) list
    3.32 +  (string * (Proof.context -> term list -> term)) list
    3.33  val typed_print_translation:
    3.34 -  (string * (Context.generic -> bool -> typ -> term list -> term)) list
    3.35 +  (string * (Proof.context -> bool -> typ -> term list -> term)) list
    3.36  val print_ast_translation:
    3.37 -  (string * (Context.generic -> ast list -> ast)) list
    3.38 +  (string * (Proof.context -> ast list -> ast)) list
    3.39  \end{ttbox}%
    3.40  \end{isamarkuptext}%
    3.41  \isamarkuptrue%