# HG changeset patch
# User wenzelm
# Date 1288299573 -7200
# Node ID a2dde53b15efa90c47b5d6191321183815894000
# Parent  c4336e45f199c7a828422cd13b3b4247c85d2dba
tuned;

diff -r c4336e45f199 -r a2dde53b15ef doc-src/IsarRef/Thy/Spec.thy
--- 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}
diff -r c4336e45f199 -r a2dde53b15ef doc-src/IsarRef/Thy/document/Spec.tex
--- 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}