# HG changeset patch
# User wenzelm
# Date 1307390554 -7200
# Node ID 48a0a9db3453edc587fd30f7509d34424f2cd1ff
# Parent  e68c3861b8db3dfe873858129c0099bd4027f9b8
tuned;

diff -r e68c3861b8db -r 48a0a9db3453 doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Jun 06 19:13:48 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Jun 06 22:02:34 2011 +0200
@@ -295,7 +295,7 @@
 *}
 
 
-subsubsection {* Styled antiquotations *}
+subsection {* Styled antiquotations *}
 
 text {* The antiquotations @{text thm}, @{text prop} and @{text
   term} admit an extra \emph{style} specification to modify the
@@ -323,7 +323,7 @@
 *}
 
 
-subsubsection {* General options *}
+subsection {* General options *}
 
 text {* The following options are available to tune the printed output
   of antiquotations.  Note that many of these coincide with global ML
diff -r e68c3861b8db -r 48a0a9db3453 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Mon Jun 06 19:13:48 2011 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Jun 06 22:02:34 2011 +0200
@@ -2,7 +2,7 @@
 imports Base Main
 begin
 
-chapter {* Theory specifications *}
+chapter {* Specifications *}
 
 text {*
   The Isabelle/Isar theory format integrates specifications and
@@ -922,14 +922,14 @@
       Thm.rule_attribute
         (fn context: Context.generic => fn th: thm =>
           let val th' = th OF ths
-          in th' end)) *}  "my rule"
+          in th' end)) *}
 
   attribute_setup my_declaration = {*
     Attrib.thms >> (fn ths =>
       Thm.declaration_attribute
         (fn th: thm => fn context: Context.generic =>
           let val context' = context
-          in context' end)) *}  "my declaration"
+          in context' end)) *}
 
 
 section {* Primitive specification elements *}
diff -r e68c3861b8db -r 48a0a9db3453 doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Jun 06 19:13:48 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Jun 06 22:02:34 2011 +0200
@@ -446,7 +446,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Styled antiquotations%
+\isamarkupsubsection{Styled antiquotations%
 }
 \isamarkuptrue%
 %
@@ -476,7 +476,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{General options%
+\isamarkupsubsection{General options%
 }
 \isamarkuptrue%
 %
diff -r e68c3861b8db -r 48a0a9db3453 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Jun 06 19:13:48 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Jun 06 22:02:34 2011 +0200
@@ -18,7 +18,7 @@
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Theory specifications%
+\isamarkupchapter{Specifications%
 }
 \isamarkuptrue%
 %
@@ -1357,7 +1357,7 @@
 \ \ \ \ \ \ Thm{\isaliteral{2E}{\isachardot}}rule{\isaliteral{5F}{\isacharunderscore}}attribute\isanewline
 \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}fn\ context{\isaliteral{3A}{\isacharcolon}}\ Context{\isaliteral{2E}{\isachardot}}generic\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ th{\isaliteral{3A}{\isacharcolon}}\ thm\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
 \ \ \ \ \ \ \ \ \ \ let\ val\ th{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ th\ OF\ ths\isanewline
-\ \ \ \ \ \ \ \ \ \ in\ th{\isaliteral{27}{\isacharprime}}\ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ rule{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \ \ \ \ \ \ in\ th{\isaliteral{27}{\isacharprime}}\ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
 \isanewline
 \ \ \isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
 \ my{\isaliteral{5F}{\isacharunderscore}}declaration\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
@@ -1365,7 +1365,7 @@
 \ \ \ \ \ \ Thm{\isaliteral{2E}{\isachardot}}declaration{\isaliteral{5F}{\isacharunderscore}}attribute\isanewline
 \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}fn\ th{\isaliteral{3A}{\isacharcolon}}\ thm\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ context{\isaliteral{3A}{\isacharcolon}}\ Context{\isaliteral{2E}{\isachardot}}generic\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
 \ \ \ \ \ \ \ \ \ \ let\ val\ context{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ context\isanewline
-\ \ \ \ \ \ \ \ \ \ in\ context{\isaliteral{27}{\isacharprime}}\ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ declaration{\isaliteral{22}{\isachardoublequoteclose}}%
+\ \ \ \ \ \ \ \ \ \ in\ context{\isaliteral{27}{\isacharprime}}\ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
 \endisatagML
 {\isafoldML}%
 %