tuned rail diagrams and layout;
authorwenzelm
Thu May 05 23:15:11 2011 +0200 (2011-05-05)
changeset 427043f19e324ff59
parent 42703 6ab174bfefe2
child 42705 528a2ba8fa74
tuned rail diagrams and layout;
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/HOLCF_Specific.thy
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/Proof.thy
doc-src/IsarRef/Thy/Spec.thy
doc-src/IsarRef/Thy/ZF_Specific.thy
doc-src/IsarRef/Thy/document/Generic.tex
doc-src/IsarRef/Thy/document/HOLCF_Specific.tex
doc-src/IsarRef/Thy/document/HOL_Specific.tex
doc-src/IsarRef/Thy/document/Proof.tex
doc-src/IsarRef/Thy/document/Spec.tex
doc-src/IsarRef/Thy/document/ZF_Specific.tex
     1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Thu May 05 15:01:32 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Thu May 05 23:15:11 2011 +0200
     1.3 @@ -189,7 +189,7 @@
     1.4    \end{matharray}
     1.5  
     1.6    @{rail "
     1.7 -    @@{method subst} ('(' 'asm' ')')? ('(' (@{syntax nat}+) ')')? @{syntax thmref}
     1.8 +    @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}
     1.9      ;
    1.10      @@{method split} ('(' 'asm' ')')? @{syntax thmrefs}
    1.11    "}
    1.12 @@ -292,7 +292,7 @@
    1.13  
    1.14    @{rail "
    1.15      (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
    1.16 -      @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}?
    1.17 +      @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}? \\
    1.18      ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
    1.19      ;
    1.20      @@{method subgoal_tac} @{syntax goalspec}? (@{syntax prop} +)
     2.1 --- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Thu May 05 15:01:32 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Thu May 05 23:15:11 2011 +0200
     2.3 @@ -35,10 +35,10 @@
     2.4    \end{matharray}
     2.5  
     2.6    @{rail "
     2.7 -    @@{command (HOLCF) domain} @{syntax parname}? (dmspec + @'and')
     2.8 +    @@{command (HOLCF) domain} @{syntax parname}? (spec + @'and')
     2.9      ;
    2.10  
    2.11 -    dmspec: @{syntax typespec} '=' (cons + '|')
    2.12 +    spec: @{syntax typespec} '=' (cons + '|')
    2.13      ;
    2.14      cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
    2.15      ;
     3.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 05 15:01:32 2011 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 05 23:15:11 2011 +0200
     3.3 @@ -172,7 +172,8 @@
     3.4    \end{matharray}
     3.5  
     3.6    @{rail "
     3.7 -    @@{command (HOL) record} @{syntax typespecsorts} '=' (@{syntax type} '+')? (@{syntax constdecl} +)
     3.8 +    @@{command (HOL) record} @{syntax typespecsorts} '=' \\
     3.9 +      (@{syntax type} '+')? (@{syntax constdecl} +)
    3.10    "}
    3.11  
    3.12    \begin{description}
    3.13 @@ -346,12 +347,12 @@
    3.14    \end{matharray}
    3.15  
    3.16    @{rail "
    3.17 -    @@{command (HOL) datatype} (dtspec + @'and')
    3.18 +    @@{command (HOL) datatype} (spec + @'and')
    3.19      ;
    3.20      @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
    3.21      ;
    3.22  
    3.23 -    dtspec: @{syntax parname}? @{syntax typespec} @{syntax mixfix}? '=' (cons + '|')
    3.24 +    spec: @{syntax parname}? @{syntax typespec} @{syntax mixfix}? '=' (cons + '|')
    3.25      ;
    3.26      cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
    3.27    "}
     4.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Thu May 05 15:01:32 2011 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Thu May 05 23:15:11 2011 +0200
     4.3 @@ -917,19 +917,19 @@
     4.4    \end{description}
     4.5  *}
     4.6  
     4.7 -    method_setup my_method1 = {*
     4.8 -      Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))
     4.9 -    *}  "my first method (without any arguments)"
    4.10 +  method_setup my_method1 = {*
    4.11 +    Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))
    4.12 +  *}  "my first method (without any arguments)"
    4.13  
    4.14 -    method_setup my_method2 = {*
    4.15 -      Scan.succeed (fn ctxt: Proof.context =>
    4.16 -        SIMPLE_METHOD' (fn i: int => no_tac))
    4.17 -    *}  "my second method (with context)"
    4.18 +  method_setup my_method2 = {*
    4.19 +    Scan.succeed (fn ctxt: Proof.context =>
    4.20 +      SIMPLE_METHOD' (fn i: int => no_tac))
    4.21 +  *}  "my second method (with context)"
    4.22  
    4.23 -    method_setup my_method3 = {*
    4.24 -      Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
    4.25 -        SIMPLE_METHOD' (fn i: int => no_tac))
    4.26 -    *}  "my third method (with theorem arguments and context)"
    4.27 +  method_setup my_method3 = {*
    4.28 +    Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
    4.29 +      SIMPLE_METHOD' (fn i: int => no_tac))
    4.30 +  *}  "my third method (with theorem arguments and context)"
    4.31  
    4.32  
    4.33  section {* Generalized elimination \label{sec:obtain} *}
    4.34 @@ -1275,7 +1275,8 @@
    4.35    ``strengthened'' inductive statements within the object-logic.
    4.36  
    4.37    @{rail "
    4.38 -    @@{method cases} ('(' 'no_simp' ')')? (@{syntax insts} * @'and') rule?
    4.39 +    @@{method cases} ('(' 'no_simp' ')')? \\
    4.40 +      (@{syntax insts} * @'and') rule?
    4.41      ;
    4.42      @@{method induct} ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
    4.43      ;
     5.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Thu May 05 15:01:32 2011 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Thu May 05 23:15:11 2011 +0200
     5.3 @@ -51,7 +51,7 @@
     5.4    admissible.
     5.5  
     5.6    @{rail "
     5.7 -    @@{command theory} @{syntax name} @'imports' (@{syntax name} +) uses? @'begin'
     5.8 +    @@{command theory} @{syntax name} \\ @'imports' (@{syntax name} +) uses? @'begin'
     5.9      ;
    5.10  
    5.11      uses: @'uses' ((@{syntax name} | @{syntax parname}) +)
    5.12 @@ -173,10 +173,10 @@
    5.13    @{rail "
    5.14      @@{command axiomatization} @{syntax \"fixes\"}? (@'where' specs)?
    5.15      ;
    5.16 -    @@{command definition} @{syntax target}? (decl @'where')?
    5.17 -      @{syntax thmdecl}? @{syntax prop}
    5.18 +    @@{command definition} @{syntax target}? \\
    5.19 +      (decl @'where')? @{syntax thmdecl}? @{syntax prop}
    5.20      ;
    5.21 -    @@{command abbreviation} @{syntax target}? @{syntax mode}?
    5.22 +    @@{command abbreviation} @{syntax target}? @{syntax mode}? \\
    5.23        (decl @'where')? @{syntax prop}
    5.24      ;
    5.25  
    5.26 @@ -259,7 +259,7 @@
    5.27  
    5.28    @{rail "
    5.29      (@@{command declaration} | @@{command syntax_declaration})
    5.30 -      ('(' @'pervasive' ')')? @{syntax target}? @{syntax text}
    5.31 +      ('(' @'pervasive' ')')? \\ @{syntax target}? @{syntax text}
    5.32      ;
    5.33      @@{command declare} @{syntax target}? (@{syntax thmrefs} + @'and')
    5.34    "}
    5.35 @@ -503,7 +503,8 @@
    5.36      ;
    5.37      @@{command interpret} @{syntax locale_expr} equations?
    5.38      ;
    5.39 -    @@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax locale_expr} equations?
    5.40 +    @@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax locale_expr} \\
    5.41 +      equations?
    5.42      ;
    5.43      @@{command print_dependencies} '!'? @{syntax locale_expr}
    5.44      ;
    5.45 @@ -639,25 +640,18 @@
    5.46    \end{matharray}
    5.47  
    5.48    @{rail "
    5.49 -    @@{command class} @{syntax name} '='
    5.50 +    @@{command class} class_spec @'begin'?
    5.51 +    ;
    5.52 +    class_spec: @{syntax name} '='
    5.53        ((@{syntax nameref} '+' (@{syntax context_elem}+)) |
    5.54 -        @{syntax nameref} | (@{syntax context_elem}+)) \\
    5.55 -      @'begin'?
    5.56 +        @{syntax nameref} | (@{syntax context_elem}+))      
    5.57      ;
    5.58      @@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin'
    5.59      ;
    5.60 -    @@{command instance}
    5.61 -    ;
    5.62 -    @@{command instance} (@{syntax nameref} + @'and') '::' @{syntax arity}
    5.63 +    @@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} |
    5.64 +      @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
    5.65      ;
    5.66      @@{command subclass} @{syntax target}? @{syntax nameref}
    5.67 -    ;
    5.68 -    @@{command instance} @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref}
    5.69 -    ;
    5.70 -    @@{command print_classes}
    5.71 -    ;
    5.72 -    @@{command class_deps}
    5.73 -    ;
    5.74    "}
    5.75  
    5.76    \begin{description}
    5.77 @@ -818,9 +812,9 @@
    5.78    \end{matharray}
    5.79  
    5.80    @{rail "
    5.81 -    @@{command overloading} \\
    5.82 -    ( @{syntax name} ( '==' | '\<equiv>' ) @{syntax term}
    5.83 -    ( '(' @'unchecked' ')' )? +) @'begin'
    5.84 +    @@{command overloading} ( spec + ) @'begin'
    5.85 +    ;
    5.86 +    spec: @{syntax name} ( '==' | '\<equiv>' ) @{syntax term} ( '(' @'unchecked' ')' )?
    5.87    "}
    5.88  
    5.89    \begin{description}
    5.90 @@ -923,15 +917,17 @@
    5.91    \end{description}
    5.92  *}
    5.93  
    5.94 -    attribute_setup my_rule = {*
    5.95 -      Attrib.thms >> (fn ths =>
    5.96 -        Thm.rule_attribute (fn context: Context.generic => fn th: thm =>
    5.97 +  attribute_setup my_rule = {*
    5.98 +    Attrib.thms >> (fn ths =>
    5.99 +      Thm.rule_attribute
   5.100 +        (fn context: Context.generic => fn th: thm =>
   5.101            let val th' = th OF ths
   5.102            in th' end)) *}  "my rule"
   5.103  
   5.104 -    attribute_setup my_declaration = {*
   5.105 -      Attrib.thms >> (fn ths =>
   5.106 -        Thm.declaration_attribute (fn th: thm => fn context: Context.generic =>
   5.107 +  attribute_setup my_declaration = {*
   5.108 +    Attrib.thms >> (fn ths =>
   5.109 +      Thm.declaration_attribute
   5.110 +        (fn th: thm => fn context: Context.generic =>
   5.111            let val context' = context
   5.112            in context' end)) *}  "my declaration"
   5.113  
   5.114 @@ -1075,8 +1071,9 @@
   5.115    @{rail "
   5.116      @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +)
   5.117      ;
   5.118 -    @@{command defs} ('(' @'unchecked'? @'overloaded'? ')')? \\
   5.119 -      (@{syntax axmdecl} @{syntax prop} +)
   5.120 +    @@{command defs} opt? (@{syntax axmdecl} @{syntax prop} +)
   5.121 +    ;
   5.122 +    opt: '(' @'unchecked'? @'overloaded'? ')'
   5.123    "}
   5.124  
   5.125    \begin{description}
     6.1 --- a/doc-src/IsarRef/Thy/ZF_Specific.thy	Thu May 05 15:01:32 2011 +0200
     6.2 +++ b/doc-src/IsarRef/Thy/ZF_Specific.thy	Thu May 05 23:15:11 2011 +0200
     6.3 @@ -62,7 +62,8 @@
     6.4      ;
     6.5      intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +)
     6.6      ;
     6.7 -    hints: @{syntax (ZF) \"monos\"}? condefs? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
     6.8 +    hints: @{syntax (ZF) \"monos\"}? condefs? \\
     6.9 +      @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
    6.10      ;
    6.11      @{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs}
    6.12      ;
     7.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Thu May 05 15:01:32 2011 +0200
     7.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Thu May 05 23:15:11 2011 +0200
     7.3 @@ -297,7 +297,7 @@
     7.4    \end{matharray}
     7.5  
     7.6    \begin{railoutput}
     7.7 -\rail@begin{3}{}
     7.8 +\rail@begin{6}{}
     7.9  \rail@term{\hyperlink{method.subst}{\mbox{\isa{subst}}}}[]
    7.10  \rail@bar
    7.11  \rail@nextbar{1}
    7.12 @@ -305,12 +305,13 @@
    7.13  \rail@term{\isa{asm}}[]
    7.14  \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
    7.15  \rail@endbar
    7.16 +\rail@cr{3}
    7.17  \rail@bar
    7.18 -\rail@nextbar{1}
    7.19 +\rail@nextbar{4}
    7.20  \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
    7.21  \rail@plus
    7.22  \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
    7.23 -\rail@nextplus{2}
    7.24 +\rail@nextplus{5}
    7.25  \rail@endplus
    7.26  \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
    7.27  \rail@endbar
    7.28 @@ -426,7 +427,7 @@
    7.29    \end{matharray}
    7.30  
    7.31    \begin{railoutput}
    7.32 -\rail@begin{6}{}
    7.33 +\rail@begin{9}{}
    7.34  \rail@bar
    7.35  \rail@term{\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
    7.36  \rail@nextbar{1}
    7.37 @@ -444,11 +445,12 @@
    7.38  \rail@nextbar{1}
    7.39  \rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
    7.40  \rail@endbar
    7.41 +\rail@cr{7}
    7.42  \rail@bar
    7.43  \rail@nont{\isa{dynamic{\isaliteral{5F}{\isacharunderscore}}insts}}[]
    7.44  \rail@term{\isa{\isakeyword{in}}}[]
    7.45  \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
    7.46 -\rail@nextbar{1}
    7.47 +\rail@nextbar{8}
    7.48  \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
    7.49  \rail@endbar
    7.50  \rail@end
     8.1 --- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Thu May 05 15:01:32 2011 +0200
     8.2 +++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Thu May 05 23:15:11 2011 +0200
     8.3 @@ -62,12 +62,12 @@
     8.4  \rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
     8.5  \rail@endbar
     8.6  \rail@plus
     8.7 -\rail@nont{\isa{dmspec}}[]
     8.8 +\rail@nont{\isa{spec}}[]
     8.9  \rail@nextplus{1}
    8.10  \rail@cterm{\isa{\isakeyword{and}}}[]
    8.11  \rail@endplus
    8.12  \rail@end
    8.13 -\rail@begin{2}{\isa{dmspec}}
    8.14 +\rail@begin{2}{\isa{spec}}
    8.15  \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
    8.16  \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
    8.17  \rail@plus
     9.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 05 15:01:32 2011 +0200
     9.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 05 23:15:11 2011 +0200
     9.3 @@ -237,18 +237,19 @@
     9.4    \end{matharray}
     9.5  
     9.6    \begin{railoutput}
     9.7 -\rail@begin{2}{}
     9.8 +\rail@begin{4}{}
     9.9  \rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
    9.10  \rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
    9.11  \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
    9.12 +\rail@cr{2}
    9.13  \rail@bar
    9.14 -\rail@nextbar{1}
    9.15 +\rail@nextbar{3}
    9.16  \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
    9.17  \rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
    9.18  \rail@endbar
    9.19  \rail@plus
    9.20  \rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
    9.21 -\rail@nextplus{1}
    9.22 +\rail@nextplus{3}
    9.23  \rail@endplus
    9.24  \rail@end
    9.25  \end{railoutput}
    9.26 @@ -413,7 +414,7 @@
    9.27  \rail@begin{2}{}
    9.28  \rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
    9.29  \rail@plus
    9.30 -\rail@nont{\isa{dtspec}}[]
    9.31 +\rail@nont{\isa{spec}}[]
    9.32  \rail@nextplus{1}
    9.33  \rail@cterm{\isa{\isakeyword{and}}}[]
    9.34  \rail@endplus
    9.35 @@ -434,7 +435,7 @@
    9.36  \rail@nextplus{1}
    9.37  \rail@endplus
    9.38  \rail@end
    9.39 -\rail@begin{2}{\isa{dtspec}}
    9.40 +\rail@begin{2}{\isa{spec}}
    9.41  \rail@bar
    9.42  \rail@nextbar{1}
    9.43  \rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
    10.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Thu May 05 15:01:32 2011 +0200
    10.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Thu May 05 23:15:11 2011 +0200
    10.3 @@ -1260,26 +1260,26 @@
    10.4  \isamarkuptrue%
    10.5  %
    10.6  \isadelimML
    10.7 -\ \ \ \ %
    10.8 +\ \ %
    10.9  \endisadelimML
   10.10  %
   10.11  \isatagML
   10.12  \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
   10.13  \ my{\isaliteral{5F}{\isacharunderscore}}method{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   10.14 -\ \ \ \ \ \ 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
   10.15 -\ \ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ first\ method\ {\isaliteral{28}{\isacharparenleft}}without\ any\ arguments{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   10.16 +\ \ \ \ 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
   10.17 +\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ first\ method\ {\isaliteral{28}{\isacharparenleft}}without\ any\ arguments{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   10.18  \isanewline
   10.19 -\ \ \ \ \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
   10.20 +\ \ \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
   10.21  \ my{\isaliteral{5F}{\isacharunderscore}}method{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   10.22 -\ \ \ \ \ \ 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
   10.23 -\ \ \ \ \ \ \ \ 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
   10.24 -\ \ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ second\ method\ {\isaliteral{28}{\isacharparenleft}}with\ context{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   10.25 +\ \ \ \ 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
   10.26 +\ \ \ \ \ \ 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
   10.27 +\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ second\ method\ {\isaliteral{28}{\isacharparenleft}}with\ context{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   10.28  \isanewline
   10.29 -\ \ \ \ \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
   10.30 +\ \ \isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
   10.31  \ my{\isaliteral{5F}{\isacharunderscore}}method{\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   10.32 -\ \ \ \ \ \ 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
   10.33 -\ \ \ \ \ \ \ \ 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
   10.34 -\ \ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ third\ method\ {\isaliteral{28}{\isacharparenleft}}with\ theorem\ arguments\ and\ context{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
   10.35 +\ \ \ \ 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
   10.36 +\ \ \ \ \ \ 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
   10.37 +\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ third\ method\ {\isaliteral{28}{\isacharparenleft}}with\ theorem\ arguments\ and\ context{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
   10.38  \endisatagML
   10.39  {\isafoldML}%
   10.40  %
   10.41 @@ -1700,7 +1700,7 @@
   10.42    ``strengthened'' inductive statements within the object-logic.
   10.43  
   10.44    \begin{railoutput}
   10.45 -\rail@begin{3}{}
   10.46 +\rail@begin{6}{}
   10.47  \rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
   10.48  \rail@bar
   10.49  \rail@nextbar{1}
   10.50 @@ -1708,16 +1708,17 @@
   10.51  \rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}simp}}[]
   10.52  \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
   10.53  \rail@endbar
   10.54 +\rail@cr{3}
   10.55  \rail@bar
   10.56 -\rail@nextbar{1}
   10.57 +\rail@nextbar{4}
   10.58  \rail@plus
   10.59  \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
   10.60 -\rail@nextplus{2}
   10.61 +\rail@nextplus{5}
   10.62  \rail@cterm{\isa{\isakeyword{and}}}[]
   10.63  \rail@endplus
   10.64  \rail@endbar
   10.65  \rail@bar
   10.66 -\rail@nextbar{1}
   10.67 +\rail@nextbar{4}
   10.68  \rail@nont{\isa{rule}}[]
   10.69  \rail@endbar
   10.70  \rail@end
    11.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu May 05 15:01:32 2011 +0200
    11.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Thu May 05 23:15:11 2011 +0200
    11.3 @@ -69,16 +69,17 @@
    11.4    admissible.
    11.5  
    11.6    \begin{railoutput}
    11.7 -\rail@begin{2}{}
    11.8 +\rail@begin{4}{}
    11.9  \rail@term{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}}[]
   11.10  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
   11.11 +\rail@cr{2}
   11.12  \rail@term{\isa{\isakeyword{imports}}}[]
   11.13  \rail@plus
   11.14  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
   11.15 -\rail@nextplus{1}
   11.16 +\rail@nextplus{3}
   11.17  \rail@endplus
   11.18  \rail@bar
   11.19 -\rail@nextbar{1}
   11.20 +\rail@nextbar{3}
   11.21  \rail@nont{\isa{uses}}[]
   11.22  \rail@endbar
   11.23  \rail@term{\isa{\isakeyword{begin}}}[]
   11.24 @@ -232,24 +233,25 @@
   11.25  \rail@nont{\isa{specs}}[]
   11.26  \rail@endbar
   11.27  \rail@end
   11.28 -\rail@begin{2}{}
   11.29 +\rail@begin{5}{}
   11.30  \rail@term{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}[]
   11.31  \rail@bar
   11.32  \rail@nextbar{1}
   11.33  \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
   11.34  \rail@endbar
   11.35 +\rail@cr{3}
   11.36  \rail@bar
   11.37 -\rail@nextbar{1}
   11.38 +\rail@nextbar{4}
   11.39  \rail@nont{\isa{decl}}[]
   11.40  \rail@term{\isa{\isakeyword{where}}}[]
   11.41  \rail@endbar
   11.42  \rail@bar
   11.43 -\rail@nextbar{1}
   11.44 +\rail@nextbar{4}
   11.45  \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
   11.46  \rail@endbar
   11.47  \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
   11.48  \rail@end
   11.49 -\rail@begin{2}{}
   11.50 +\rail@begin{5}{}
   11.51  \rail@term{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}}[]
   11.52  \rail@bar
   11.53  \rail@nextbar{1}
   11.54 @@ -259,8 +261,9 @@
   11.55  \rail@nextbar{1}
   11.56  \rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[]
   11.57  \rail@endbar
   11.58 +\rail@cr{3}
   11.59  \rail@bar
   11.60 -\rail@nextbar{1}
   11.61 +\rail@nextbar{4}
   11.62  \rail@nont{\isa{decl}}[]
   11.63  \rail@term{\isa{\isakeyword{where}}}[]
   11.64  \rail@endbar
   11.65 @@ -383,7 +386,7 @@
   11.66    \end{matharray}
   11.67  
   11.68    \begin{railoutput}
   11.69 -\rail@begin{2}{}
   11.70 +\rail@begin{5}{}
   11.71  \rail@bar
   11.72  \rail@term{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}}[]
   11.73  \rail@nextbar{1}
   11.74 @@ -395,8 +398,9 @@
   11.75  \rail@term{\isa{\isakeyword{pervasive}}}[]
   11.76  \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
   11.77  \rail@endbar
   11.78 +\rail@cr{3}
   11.79  \rail@bar
   11.80 -\rail@nextbar{1}
   11.81 +\rail@nextbar{4}
   11.82  \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
   11.83  \rail@endbar
   11.84  \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
   11.85 @@ -799,7 +803,7 @@
   11.86  \rail@nont{\isa{equations}}[]
   11.87  \rail@endbar
   11.88  \rail@end
   11.89 -\rail@begin{2}{}
   11.90 +\rail@begin{5}{}
   11.91  \rail@term{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}}[]
   11.92  \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
   11.93  \rail@bar
   11.94 @@ -808,8 +812,9 @@
   11.95  \rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
   11.96  \rail@endbar
   11.97  \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
   11.98 +\rail@cr{3}
   11.99  \rail@bar
  11.100 -\rail@nextbar{1}
  11.101 +\rail@nextbar{4}
  11.102  \rail@nont{\isa{equations}}[]
  11.103  \rail@endbar
  11.104  \rail@end
  11.105 @@ -965,8 +970,15 @@
  11.106    \end{matharray}
  11.107  
  11.108    \begin{railoutput}
  11.109 -\rail@begin{8}{}
  11.110 +\rail@begin{2}{}
  11.111  \rail@term{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}}[]
  11.112 +\rail@nont{\isa{class{\isaliteral{5F}{\isacharunderscore}}spec}}[]
  11.113 +\rail@bar
  11.114 +\rail@nextbar{1}
  11.115 +\rail@term{\isa{\isakeyword{begin}}}[]
  11.116 +\rail@endbar
  11.117 +\rail@end
  11.118 +\rail@begin{5}{\isa{class{\isaliteral{5F}{\isacharunderscore}}spec}}
  11.119  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  11.120  \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
  11.121  \rail@bar
  11.122 @@ -984,11 +996,6 @@
  11.123  \rail@nextplus{4}
  11.124  \rail@endplus
  11.125  \rail@endbar
  11.126 -\rail@cr{6}
  11.127 -\rail@bar
  11.128 -\rail@nextbar{7}
  11.129 -\rail@term{\isa{\isakeyword{begin}}}[]
  11.130 -\rail@endbar
  11.131  \rail@end
  11.132  \rail@begin{2}{}
  11.133  \rail@term{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}}[]
  11.134 @@ -1001,18 +1008,26 @@
  11.135  \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
  11.136  \rail@term{\isa{\isakeyword{begin}}}[]
  11.137  \rail@end
  11.138 -\rail@begin{1}{}
  11.139 +\rail@begin{5}{}
  11.140  \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
  11.141 -\rail@end
  11.142 -\rail@begin{2}{}
  11.143 -\rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
  11.144 +\rail@bar
  11.145 +\rail@nextbar{1}
  11.146  \rail@plus
  11.147  \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  11.148 -\rail@nextplus{1}
  11.149 +\rail@nextplus{2}
  11.150  \rail@cterm{\isa{\isakeyword{and}}}[]
  11.151  \rail@endplus
  11.152  \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
  11.153  \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
  11.154 +\rail@nextbar{3}
  11.155 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  11.156 +\rail@bar
  11.157 +\rail@term{\isa{{\isaliteral{3C}{\isacharless}}}}[]
  11.158 +\rail@nextbar{4}
  11.159 +\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
  11.160 +\rail@endbar
  11.161 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  11.162 +\rail@endbar
  11.163  \rail@end
  11.164  \rail@begin{2}{}
  11.165  \rail@term{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}}[]
  11.166 @@ -1022,22 +1037,6 @@
  11.167  \rail@endbar
  11.168  \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  11.169  \rail@end
  11.170 -\rail@begin{2}{}
  11.171 -\rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
  11.172 -\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  11.173 -\rail@bar
  11.174 -\rail@term{\isa{{\isaliteral{3C}{\isacharless}}}}[]
  11.175 -\rail@nextbar{1}
  11.176 -\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
  11.177 -\rail@endbar
  11.178 -\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  11.179 -\rail@end
  11.180 -\rail@begin{1}{}
  11.181 -\rail@term{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}}[]
  11.182 -\rail@end
  11.183 -\rail@begin{1}{}
  11.184 -\rail@term{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
  11.185 -\rail@end
  11.186  \end{railoutput}
  11.187  
  11.188  
  11.189 @@ -1197,26 +1196,28 @@
  11.190    \end{matharray}
  11.191  
  11.192    \begin{railoutput}
  11.193 -\rail@begin{5}{}
  11.194 +\rail@begin{2}{}
  11.195  \rail@term{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}}[]
  11.196 -\rail@cr{2}
  11.197  \rail@plus
  11.198 +\rail@nont{\isa{spec}}[]
  11.199 +\rail@nextplus{1}
  11.200 +\rail@endplus
  11.201 +\rail@term{\isa{\isakeyword{begin}}}[]
  11.202 +\rail@end
  11.203 +\rail@begin{2}{\isa{spec}}
  11.204  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  11.205  \rail@bar
  11.206  \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}}}[]
  11.207 -\rail@nextbar{3}
  11.208 +\rail@nextbar{1}
  11.209  \rail@term{\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}}[]
  11.210  \rail@endbar
  11.211  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
  11.212  \rail@bar
  11.213 -\rail@nextbar{3}
  11.214 +\rail@nextbar{1}
  11.215  \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
  11.216  \rail@term{\isa{\isakeyword{unchecked}}}[]
  11.217  \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
  11.218  \rail@endbar
  11.219 -\rail@nextplus{4}
  11.220 -\rail@endplus
  11.221 -\rail@term{\isa{\isakeyword{begin}}}[]
  11.222  \rail@end
  11.223  \end{railoutput}
  11.224  
  11.225 @@ -1343,21 +1344,23 @@
  11.226  \isamarkuptrue%
  11.227  %
  11.228  \isadelimML
  11.229 -\ \ \ \ %
  11.230 +\ \ %
  11.231  \endisadelimML
  11.232  %
  11.233  \isatagML
  11.234  \isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
  11.235  \ my{\isaliteral{5F}{\isacharunderscore}}rule\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  11.236 -\ \ \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ ths\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
  11.237 -\ \ \ \ \ \ \ \ 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
  11.238 +\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ ths\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
  11.239 +\ \ \ \ \ \ Thm{\isaliteral{2E}{\isachardot}}rule{\isaliteral{5F}{\isacharunderscore}}attribute\isanewline
  11.240 +\ \ \ \ \ \ \ \ {\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
  11.241  \ \ \ \ \ \ \ \ \ \ let\ val\ th{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ th\ OF\ ths\isanewline
  11.242  \ \ \ \ \ \ \ \ \ \ in\ th{\isaliteral{27}{\isacharprime}}\ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ rule{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
  11.243  \isanewline
  11.244 -\ \ \ \ \isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
  11.245 +\ \ \isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
  11.246  \ my{\isaliteral{5F}{\isacharunderscore}}declaration\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  11.247 -\ \ \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ ths\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
  11.248 -\ \ \ \ \ \ \ \ 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
  11.249 +\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ ths\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
  11.250 +\ \ \ \ \ \ Thm{\isaliteral{2E}{\isachardot}}declaration{\isaliteral{5F}{\isacharunderscore}}attribute\isanewline
  11.251 +\ \ \ \ \ \ \ \ {\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
  11.252  \ \ \ \ \ \ \ \ \ \ let\ val\ context{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ context\isanewline
  11.253  \ \ \ \ \ \ \ \ \ \ in\ context{\isaliteral{27}{\isacharprime}}\ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ declaration{\isaliteral{22}{\isachardoublequoteclose}}%
  11.254  \endisatagML
  11.255 @@ -1566,27 +1569,29 @@
  11.256  \rail@nextplus{2}
  11.257  \rail@endplus
  11.258  \rail@end
  11.259 -\rail@begin{6}{}
  11.260 +\rail@begin{2}{}
  11.261  \rail@term{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}}[]
  11.262  \rail@bar
  11.263  \rail@nextbar{1}
  11.264 +\rail@nont{\isa{opt}}[]
  11.265 +\rail@endbar
  11.266 +\rail@plus
  11.267 +\rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[]
  11.268 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
  11.269 +\rail@nextplus{1}
  11.270 +\rail@endplus
  11.271 +\rail@end
  11.272 +\rail@begin{2}{\isa{opt}}
  11.273  \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
  11.274  \rail@bar
  11.275 -\rail@nextbar{2}
  11.276 +\rail@nextbar{1}
  11.277  \rail@term{\isa{\isakeyword{unchecked}}}[]
  11.278  \rail@endbar
  11.279  \rail@bar
  11.280 -\rail@nextbar{2}
  11.281 +\rail@nextbar{1}
  11.282  \rail@term{\isa{\isakeyword{overloaded}}}[]
  11.283  \rail@endbar
  11.284  \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
  11.285 -\rail@endbar
  11.286 -\rail@cr{4}
  11.287 -\rail@plus
  11.288 -\rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[]
  11.289 -\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
  11.290 -\rail@nextplus{5}
  11.291 -\rail@endplus
  11.292  \rail@end
  11.293  \end{railoutput}
  11.294  
    12.1 --- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Thu May 05 15:01:32 2011 +0200
    12.2 +++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Thu May 05 23:15:11 2011 +0200
    12.3 @@ -123,7 +123,7 @@
    12.4  \rail@nextplus{2}
    12.5  \rail@endplus
    12.6  \rail@end
    12.7 -\rail@begin{2}{\isa{hints}}
    12.8 +\rail@begin{5}{\isa{hints}}
    12.9  \rail@bar
   12.10  \rail@nextbar{1}
   12.11  \rail@nont{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}[]
   12.12 @@ -132,12 +132,13 @@
   12.13  \rail@nextbar{1}
   12.14  \rail@nont{\isa{condefs}}[]
   12.15  \rail@endbar
   12.16 +\rail@cr{3}
   12.17  \rail@bar
   12.18 -\rail@nextbar{1}
   12.19 +\rail@nextbar{4}
   12.20  \rail@nont{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}[]
   12.21  \rail@endbar
   12.22  \rail@bar
   12.23 -\rail@nextbar{1}
   12.24 +\rail@nextbar{4}
   12.25  \rail@nont{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}[]
   12.26  \rail@endbar
   12.27  \rail@end