--- 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
--- 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 *}
--- 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%
%
--- 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}%
%