--- a/doc-src/IsarRef/Thy/Spec.thy Thu Oct 28 22:39:59 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Thu Oct 28 22:59:33 2010 +0200
@@ -159,7 +159,7 @@
text {*
\begin{matharray}{rcll}
- @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!)\\
+ @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
@{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{attribute_def "defn"} & : & @{text attribute} \\
@{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@@ -1139,8 +1139,8 @@
asserted, and records within the internal derivation object how
presumed theorems depend on unproven suppositions.
- \begin{matharray}{rcl}
- @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} \\
+ \begin{matharray}{rcll}
+ @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
\end{matharray}
\begin{rail}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Oct 28 22:39:59 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Oct 28 22:59:33 2010 +0200
@@ -179,7 +179,7 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcll}
- \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!)\\
+ \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
\indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
\indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isa{attribute} \\
\indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
@@ -1179,8 +1179,8 @@
asserted, and records within the internal derivation object how
presumed theorems depend on unproven suppositions.
- \begin{matharray}{rcl}
- \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \begin{matharray}{rcll}
+ \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
\end{matharray}
\begin{rail}