--- 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} +)
--- 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}?
;
--- 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}?
"}
--- 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?
;
--- 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}
--- 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}
;
--- 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
--- 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
--- 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}}}}[]
--- 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
--- 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}
--- 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