# HG changeset patch
# User wenzelm
# Date 1304630111 -7200
# Node ID 3f19e324ff59be4cfdd20ced01789d98afe15e90
# Parent  6ab174bfefe296b4f674084ad5e97a8d5fca119f
tuned rail diagrams and layout;

diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Thu May 05 15:01:32 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Thu May 05 23:15:11 2011 +0200
@@ -189,7 +189,7 @@
   \end{matharray}
 
   @{rail "
-    @@{method subst} ('(' 'asm' ')')? ('(' (@{syntax nat}+) ')')? @{syntax thmref}
+    @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}
     ;
     @@{method split} ('(' 'asm' ')')? @{syntax thmrefs}
   "}
@@ -292,7 +292,7 @@
 
   @{rail "
     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
-      @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}?
+      @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}? \\
     ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
     ;
     @@{method subgoal_tac} @{syntax goalspec}? (@{syntax prop} +)
diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/HOLCF_Specific.thy
--- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Thu May 05 15:01:32 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Thu May 05 23:15:11 2011 +0200
@@ -35,10 +35,10 @@
   \end{matharray}
 
   @{rail "
-    @@{command (HOLCF) domain} @{syntax parname}? (dmspec + @'and')
+    @@{command (HOLCF) domain} @{syntax parname}? (spec + @'and')
     ;
 
-    dmspec: @{syntax typespec} '=' (cons + '|')
+    spec: @{syntax typespec} '=' (cons + '|')
     ;
     cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
     ;
diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 05 15:01:32 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 05 23:15:11 2011 +0200
@@ -172,7 +172,8 @@
   \end{matharray}
 
   @{rail "
-    @@{command (HOL) record} @{syntax typespecsorts} '=' (@{syntax type} '+')? (@{syntax constdecl} +)
+    @@{command (HOL) record} @{syntax typespecsorts} '=' \\
+      (@{syntax type} '+')? (@{syntax constdecl} +)
   "}
 
   \begin{description}
@@ -346,12 +347,12 @@
   \end{matharray}
 
   @{rail "
-    @@{command (HOL) datatype} (dtspec + @'and')
+    @@{command (HOL) datatype} (spec + @'and')
     ;
     @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
     ;
 
-    dtspec: @{syntax parname}? @{syntax typespec} @{syntax mixfix}? '=' (cons + '|')
+    spec: @{syntax parname}? @{syntax typespec} @{syntax mixfix}? '=' (cons + '|')
     ;
     cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
   "}
diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Thu May 05 15:01:32 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Thu May 05 23:15:11 2011 +0200
@@ -917,19 +917,19 @@
   \end{description}
 *}
 
-    method_setup my_method1 = {*
-      Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))
-    *}  "my first method (without any arguments)"
+  method_setup my_method1 = {*
+    Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))
+  *}  "my first method (without any arguments)"
 
-    method_setup my_method2 = {*
-      Scan.succeed (fn ctxt: Proof.context =>
-        SIMPLE_METHOD' (fn i: int => no_tac))
-    *}  "my second method (with context)"
+  method_setup my_method2 = {*
+    Scan.succeed (fn ctxt: Proof.context =>
+      SIMPLE_METHOD' (fn i: int => no_tac))
+  *}  "my second method (with context)"
 
-    method_setup my_method3 = {*
-      Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
-        SIMPLE_METHOD' (fn i: int => no_tac))
-    *}  "my third method (with theorem arguments and context)"
+  method_setup my_method3 = {*
+    Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
+      SIMPLE_METHOD' (fn i: int => no_tac))
+  *}  "my third method (with theorem arguments and context)"
 
 
 section {* Generalized elimination \label{sec:obtain} *}
@@ -1275,7 +1275,8 @@
   ``strengthened'' inductive statements within the object-logic.
 
   @{rail "
-    @@{method cases} ('(' 'no_simp' ')')? (@{syntax insts} * @'and') rule?
+    @@{method cases} ('(' 'no_simp' ')')? \\
+      (@{syntax insts} * @'and') rule?
     ;
     @@{method induct} ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
     ;
diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Thu May 05 15:01:32 2011 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Thu May 05 23:15:11 2011 +0200
@@ -51,7 +51,7 @@
   admissible.
 
   @{rail "
-    @@{command theory} @{syntax name} @'imports' (@{syntax name} +) uses? @'begin'
+    @@{command theory} @{syntax name} \\ @'imports' (@{syntax name} +) uses? @'begin'
     ;
 
     uses: @'uses' ((@{syntax name} | @{syntax parname}) +)
@@ -173,10 +173,10 @@
   @{rail "
     @@{command axiomatization} @{syntax \"fixes\"}? (@'where' specs)?
     ;
-    @@{command definition} @{syntax target}? (decl @'where')?
-      @{syntax thmdecl}? @{syntax prop}
+    @@{command definition} @{syntax target}? \\
+      (decl @'where')? @{syntax thmdecl}? @{syntax prop}
     ;
-    @@{command abbreviation} @{syntax target}? @{syntax mode}?
+    @@{command abbreviation} @{syntax target}? @{syntax mode}? \\
       (decl @'where')? @{syntax prop}
     ;
 
@@ -259,7 +259,7 @@
 
   @{rail "
     (@@{command declaration} | @@{command syntax_declaration})
-      ('(' @'pervasive' ')')? @{syntax target}? @{syntax text}
+      ('(' @'pervasive' ')')? \\ @{syntax target}? @{syntax text}
     ;
     @@{command declare} @{syntax target}? (@{syntax thmrefs} + @'and')
   "}
@@ -503,7 +503,8 @@
     ;
     @@{command interpret} @{syntax locale_expr} equations?
     ;
-    @@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax locale_expr} equations?
+    @@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax locale_expr} \\
+      equations?
     ;
     @@{command print_dependencies} '!'? @{syntax locale_expr}
     ;
@@ -639,25 +640,18 @@
   \end{matharray}
 
   @{rail "
-    @@{command class} @{syntax name} '='
+    @@{command class} class_spec @'begin'?
+    ;
+    class_spec: @{syntax name} '='
       ((@{syntax nameref} '+' (@{syntax context_elem}+)) |
-        @{syntax nameref} | (@{syntax context_elem}+)) \\
-      @'begin'?
+        @{syntax nameref} | (@{syntax context_elem}+))      
     ;
     @@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin'
     ;
-    @@{command instance}
-    ;
-    @@{command instance} (@{syntax nameref} + @'and') '::' @{syntax arity}
+    @@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} |
+      @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
     ;
     @@{command subclass} @{syntax target}? @{syntax nameref}
-    ;
-    @@{command instance} @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref}
-    ;
-    @@{command print_classes}
-    ;
-    @@{command class_deps}
-    ;
   "}
 
   \begin{description}
@@ -818,9 +812,9 @@
   \end{matharray}
 
   @{rail "
-    @@{command overloading} \\
-    ( @{syntax name} ( '==' | '\<equiv>' ) @{syntax term}
-    ( '(' @'unchecked' ')' )? +) @'begin'
+    @@{command overloading} ( spec + ) @'begin'
+    ;
+    spec: @{syntax name} ( '==' | '\<equiv>' ) @{syntax term} ( '(' @'unchecked' ')' )?
   "}
 
   \begin{description}
@@ -923,15 +917,17 @@
   \end{description}
 *}
 
-    attribute_setup my_rule = {*
-      Attrib.thms >> (fn ths =>
-        Thm.rule_attribute (fn context: Context.generic => fn th: thm =>
+  attribute_setup my_rule = {*
+    Attrib.thms >> (fn ths =>
+      Thm.rule_attribute
+        (fn context: Context.generic => fn th: thm =>
           let val th' = th OF ths
           in th' end)) *}  "my rule"
 
-    attribute_setup my_declaration = {*
-      Attrib.thms >> (fn ths =>
-        Thm.declaration_attribute (fn th: thm => fn context: Context.generic =>
+  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"
 
@@ -1075,8 +1071,9 @@
   @{rail "
     @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +)
     ;
-    @@{command defs} ('(' @'unchecked'? @'overloaded'? ')')? \\
-      (@{syntax axmdecl} @{syntax prop} +)
+    @@{command defs} opt? (@{syntax axmdecl} @{syntax prop} +)
+    ;
+    opt: '(' @'unchecked'? @'overloaded'? ')'
   "}
 
   \begin{description}
diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/ZF_Specific.thy
--- a/doc-src/IsarRef/Thy/ZF_Specific.thy	Thu May 05 15:01:32 2011 +0200
+++ b/doc-src/IsarRef/Thy/ZF_Specific.thy	Thu May 05 23:15:11 2011 +0200
@@ -62,7 +62,8 @@
     ;
     intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +)
     ;
-    hints: @{syntax (ZF) \"monos\"}? condefs? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
+    hints: @{syntax (ZF) \"monos\"}? condefs? \\
+      @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
     ;
     @{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs}
     ;
diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Thu May 05 15:01:32 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Thu May 05 23:15:11 2011 +0200
@@ -297,7 +297,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{3}{}
+\rail@begin{6}{}
 \rail@term{\hyperlink{method.subst}{\mbox{\isa{subst}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -305,12 +305,13 @@
 \rail@term{\isa{asm}}[]
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@endbar
+\rail@cr{3}
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{4}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
-\rail@nextplus{2}
+\rail@nextplus{5}
 \rail@endplus
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@endbar
@@ -426,7 +427,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{6}{}
+\rail@begin{9}{}
 \rail@bar
 \rail@term{\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@nextbar{1}
@@ -444,11 +445,12 @@
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
 \rail@endbar
+\rail@cr{7}
 \rail@bar
 \rail@nont{\isa{dynamic{\isaliteral{5F}{\isacharunderscore}}insts}}[]
 \rail@term{\isa{\isakeyword{in}}}[]
 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
-\rail@nextbar{1}
+\rail@nextbar{8}
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
 \rail@endbar
 \rail@end
diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/document/HOLCF_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Thu May 05 15:01:32 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Thu May 05 23:15:11 2011 +0200
@@ -62,12 +62,12 @@
 \rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
 \rail@endbar
 \rail@plus
-\rail@nont{\isa{dmspec}}[]
+\rail@nont{\isa{spec}}[]
 \rail@nextplus{1}
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{dmspec}}
+\rail@begin{2}{\isa{spec}}
 \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
 \rail@plus
diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 05 15:01:32 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 05 23:15:11 2011 +0200
@@ -237,18 +237,19 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{}
+\rail@begin{4}{}
 \rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
 \rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
+\rail@cr{2}
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{3}
 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
 \rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
 \rail@endbar
 \rail@plus
 \rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
-\rail@nextplus{1}
+\rail@nextplus{3}
 \rail@endplus
 \rail@end
 \end{railoutput}
@@ -413,7 +414,7 @@
 \rail@begin{2}{}
 \rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
 \rail@plus
-\rail@nont{\isa{dtspec}}[]
+\rail@nont{\isa{spec}}[]
 \rail@nextplus{1}
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
@@ -434,7 +435,7 @@
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{dtspec}}
+\rail@begin{2}{\isa{spec}}
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Thu May 05 15:01:32 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Thu May 05 23:15:11 2011 +0200
@@ -1260,26 +1260,26 @@
 \isamarkuptrue%
 %
 \isadelimML
-\ \ \ \ %
+\ \ %
 \endisadelimML
 %
 \isatagML
 \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
 \ my{\isaliteral{5F}{\isacharunderscore}}method{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
-\ \ \ \ \ \ Scan{\isaliteral{2E}{\isachardot}}succeed\ {\isaliteral{28}{\isacharparenleft}}K\ {\isaliteral{28}{\isacharparenleft}}SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ no{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ first\ method\ {\isaliteral{28}{\isacharparenleft}}without\ any\ arguments{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ Scan{\isaliteral{2E}{\isachardot}}succeed\ {\isaliteral{28}{\isacharparenleft}}K\ {\isaliteral{28}{\isacharparenleft}}SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ no{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ first\ method\ {\isaliteral{28}{\isacharparenleft}}without\ any\ arguments{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \isanewline
-\ \ \ \ \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
+\ \ \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
 \ my{\isaliteral{5F}{\isacharunderscore}}method{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
-\ \ \ \ \ \ Scan{\isaliteral{2E}{\isachardot}}succeed\ {\isaliteral{28}{\isacharparenleft}}fn\ ctxt{\isaliteral{3A}{\isacharcolon}}\ Proof{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
-\ \ \ \ \ \ \ \ SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ no{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ second\ method\ {\isaliteral{28}{\isacharparenleft}}with\ context{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ Scan{\isaliteral{2E}{\isachardot}}succeed\ {\isaliteral{28}{\isacharparenleft}}fn\ ctxt{\isaliteral{3A}{\isacharcolon}}\ Proof{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
+\ \ \ \ \ \ SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ no{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ second\ method\ {\isaliteral{28}{\isacharparenleft}}with\ context{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \isanewline
-\ \ \ \ \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
+\ \ \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
 \ my{\isaliteral{5F}{\isacharunderscore}}method{\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
-\ \ \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ thms{\isaliteral{3A}{\isacharcolon}}\ thm\ list\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ ctxt{\isaliteral{3A}{\isacharcolon}}\ Proof{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
-\ \ \ \ \ \ \ \ SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ no{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ third\ method\ {\isaliteral{28}{\isacharparenleft}}with\ theorem\ arguments\ and\ context{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ thms{\isaliteral{3A}{\isacharcolon}}\ thm\ list\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ ctxt{\isaliteral{3A}{\isacharcolon}}\ Proof{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
+\ \ \ \ \ \ SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ no{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ third\ method\ {\isaliteral{28}{\isacharparenleft}}with\ theorem\ arguments\ and\ context{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
 \endisatagML
 {\isafoldML}%
 %
@@ -1700,7 +1700,7 @@
   ``strengthened'' inductive statements within the object-logic.
 
   \begin{railoutput}
-\rail@begin{3}{}
+\rail@begin{6}{}
 \rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -1708,16 +1708,17 @@
 \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}simp}}[]
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@endbar
+\rail@cr{3}
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{4}
 \rail@plus
 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
-\rail@nextplus{2}
+\rail@nextplus{5}
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@endbar
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{4}
 \rail@nont{\isa{rule}}[]
 \rail@endbar
 \rail@end
diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu May 05 15:01:32 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Thu May 05 23:15:11 2011 +0200
@@ -69,16 +69,17 @@
   admissible.
 
   \begin{railoutput}
-\rail@begin{2}{}
+\rail@begin{4}{}
 \rail@term{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@cr{2}
 \rail@term{\isa{\isakeyword{imports}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextplus{1}
+\rail@nextplus{3}
 \rail@endplus
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{3}
 \rail@nont{\isa{uses}}[]
 \rail@endbar
 \rail@term{\isa{\isakeyword{begin}}}[]
@@ -232,24 +233,25 @@
 \rail@nont{\isa{specs}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{}
+\rail@begin{5}{}
 \rail@term{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
 \rail@endbar
+\rail@cr{3}
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{4}
 \rail@nont{\isa{decl}}[]
 \rail@term{\isa{\isakeyword{where}}}[]
 \rail@endbar
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{4}
 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
 \rail@endbar
 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
 \rail@end
-\rail@begin{2}{}
+\rail@begin{5}{}
 \rail@term{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}}[]
 \rail@bar
 \rail@nextbar{1}
@@ -259,8 +261,9 @@
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[]
 \rail@endbar
+\rail@cr{3}
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{4}
 \rail@nont{\isa{decl}}[]
 \rail@term{\isa{\isakeyword{where}}}[]
 \rail@endbar
@@ -383,7 +386,7 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{2}{}
+\rail@begin{5}{}
 \rail@bar
 \rail@term{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}}[]
 \rail@nextbar{1}
@@ -395,8 +398,9 @@
 \rail@term{\isa{\isakeyword{pervasive}}}[]
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@endbar
+\rail@cr{3}
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{4}
 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
 \rail@endbar
 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
@@ -799,7 +803,7 @@
 \rail@nont{\isa{equations}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{}
+\rail@begin{5}{}
 \rail@term{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}}[]
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
 \rail@bar
@@ -808,8 +812,9 @@
 \rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
 \rail@endbar
 \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
+\rail@cr{3}
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{4}
 \rail@nont{\isa{equations}}[]
 \rail@endbar
 \rail@end
@@ -965,8 +970,15 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{8}{}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}}[]
+\rail@nont{\isa{class{\isaliteral{5F}{\isacharunderscore}}spec}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{\isakeyword{begin}}}[]
+\rail@endbar
+\rail@end
+\rail@begin{5}{\isa{class{\isaliteral{5F}{\isacharunderscore}}spec}}
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
 \rail@bar
@@ -984,11 +996,6 @@
 \rail@nextplus{4}
 \rail@endplus
 \rail@endbar
-\rail@cr{6}
-\rail@bar
-\rail@nextbar{7}
-\rail@term{\isa{\isakeyword{begin}}}[]
-\rail@endbar
 \rail@end
 \rail@begin{2}{}
 \rail@term{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}}[]
@@ -1001,18 +1008,26 @@
 \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
 \rail@term{\isa{\isakeyword{begin}}}[]
 \rail@end
-\rail@begin{1}{}
+\rail@begin{5}{}
 \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
-\rail@end
-\rail@begin{2}{}
-\rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
+\rail@bar
+\rail@nextbar{1}
 \rail@plus
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
-\rail@nextplus{1}
+\rail@nextplus{2}
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
 \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
+\rail@nextbar{3}
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
+\rail@bar
+\rail@term{\isa{{\isaliteral{3C}{\isacharless}}}}[]
+\rail@nextbar{4}
+\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
+\rail@endbar
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
+\rail@endbar
 \rail@end
 \rail@begin{2}{}
 \rail@term{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}}[]
@@ -1022,22 +1037,6 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
 \rail@end
-\rail@begin{2}{}
-\rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
-\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
-\rail@bar
-\rail@term{\isa{{\isaliteral{3C}{\isacharless}}}}[]
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
-\rail@end
-\rail@begin{1}{}
-\rail@term{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}}[]
-\rail@end
-\rail@begin{1}{}
-\rail@term{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
-\rail@end
 \end{railoutput}
 
 
@@ -1197,26 +1196,28 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{5}{}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}}[]
-\rail@cr{2}
 \rail@plus
+\rail@nont{\isa{spec}}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@term{\isa{\isakeyword{begin}}}[]
+\rail@end
+\rail@begin{2}{\isa{spec}}
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@bar
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}}}[]
-\rail@nextbar{3}
+\rail@nextbar{1}
 \rail@term{\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}}[]
 \rail@endbar
 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
 \rail@bar
-\rail@nextbar{3}
+\rail@nextbar{1}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@term{\isa{\isakeyword{unchecked}}}[]
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@endbar
-\rail@nextplus{4}
-\rail@endplus
-\rail@term{\isa{\isakeyword{begin}}}[]
 \rail@end
 \end{railoutput}
 
@@ -1343,21 +1344,23 @@
 \isamarkuptrue%
 %
 \isadelimML
-\ \ \ \ %
+\ \ %
 \endisadelimML
 %
 \isatagML
 \isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
 \ my{\isaliteral{5F}{\isacharunderscore}}rule\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
-\ \ \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ ths\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
-\ \ \ \ \ \ \ \ Thm{\isaliteral{2E}{\isachardot}}rule{\isaliteral{5F}{\isacharunderscore}}attribute\ {\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
+\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ ths\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
+\ \ \ \ \ \ 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
 \isanewline
-\ \ \ \ \isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
+\ \ \isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
 \ my{\isaliteral{5F}{\isacharunderscore}}declaration\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
-\ \ \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ ths\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
-\ \ \ \ \ \ \ \ Thm{\isaliteral{2E}{\isachardot}}declaration{\isaliteral{5F}{\isacharunderscore}}attribute\ {\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
+\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ ths\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
+\ \ \ \ \ \ 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}}%
 \endisatagML
@@ -1566,27 +1569,29 @@
 \rail@nextplus{2}
 \rail@endplus
 \rail@end
-\rail@begin{6}{}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}}[]
 \rail@bar
 \rail@nextbar{1}
+\rail@nont{\isa{opt}}[]
+\rail@endbar
+\rail@plus
+\rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[]
+\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\rail@begin{2}{\isa{opt}}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@bar
-\rail@nextbar{2}
+\rail@nextbar{1}
 \rail@term{\isa{\isakeyword{unchecked}}}[]
 \rail@endbar
 \rail@bar
-\rail@nextbar{2}
+\rail@nextbar{1}
 \rail@term{\isa{\isakeyword{overloaded}}}[]
 \rail@endbar
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@endbar
-\rail@cr{4}
-\rail@plus
-\rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[]
-\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
-\rail@nextplus{5}
-\rail@endplus
 \rail@end
 \end{railoutput}
 
diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/document/ZF_Specific.tex
--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Thu May 05 15:01:32 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Thu May 05 23:15:11 2011 +0200
@@ -123,7 +123,7 @@
 \rail@nextplus{2}
 \rail@endplus
 \rail@end
-\rail@begin{2}{\isa{hints}}
+\rail@begin{5}{\isa{hints}}
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}[]
@@ -132,12 +132,13 @@
 \rail@nextbar{1}
 \rail@nont{\isa{condefs}}[]
 \rail@endbar
+\rail@cr{3}
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{4}
 \rail@nont{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}[]
 \rail@endbar
 \rail@bar
-\rail@nextbar{1}
+\rail@nextbar{4}
 \rail@nont{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}[]
 \rail@endbar
 \rail@end