# HG changeset patch # User wenzelm # Date 1304454499 -7200 # Node ID d34154b085797bb86f841eb6c1c0629143f215e4 # Parent 390de893659ab8d590359d6ad24cf120ff78fed4# Parent 04dfffda56712ade590891db12b456c187c824b6 merged diff -r 390de893659a -r d34154b08579 NEWS --- a/NEWS Tue May 03 21:46:49 2011 +0200 +++ b/NEWS Tue May 03 22:28:19 2011 +0200 @@ -37,12 +37,16 @@ Note that automated detection from the file-system or search path has been discontinued. INCOMPATIBILITY. -* Name space: proper configuration options "long_names", -"short_names", "unique_names" instead of former unsynchronized -references. Minor INCOMPATIBILITY, need to declare options in context -like this: - - declare [[unique_names = false]] +* Name space: former unsynchronized references are now proper +configuration options, with more conventional names: + + long_names ~> names_long + short_names ~> names_short + unique_names ~> names_unique + +Minor INCOMPATIBILITY, need to declare options in context like this: + + declare [[names_unique = false]] * Literal facts `prop` may contain dummy patterns, e.g. `_ = _`. Note that the result needs to be unique, which means fact specifications diff -r 390de893659a -r d34154b08579 doc-src/Codegen/Thy/Setup.thy --- a/doc-src/Codegen/Thy/Setup.thy Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/Codegen/Thy/Setup.thy Tue May 03 22:28:19 2011 +0200 @@ -22,6 +22,6 @@ setup {* Code_Target.set_default_code_width 74 *} -declare [[unique_names = false]] +declare [[names_unique = false]] end diff -r 390de893659a -r d34154b08579 doc-src/IsarImplementation/Thy/Logic.thy --- a/doc-src/IsarImplementation/Thy/Logic.thy Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Tue May 03 22:28:19 2011 +0200 @@ -517,14 +517,14 @@ \infer[@{text "(assume)"}]{@{text "A \ A"}}{} \] \[ - \infer[@{text "(\\intro)"}]{@{text "\ \ \x. b[x]"}}{@{text "\ \ b[x]"} & @{text "x \ \"}} + \infer[@{text "(\\intro)"}]{@{text "\ \ \x. b[x]"}}{@{text "\ \ b[x]"} & @{text "x \ \"}} \qquad - \infer[@{text "(\\elim)"}]{@{text "\ \ b[a]"}}{@{text "\ \ \x. b[x]"}} + \infer[@{text "(\\elim)"}]{@{text "\ \ b[a]"}}{@{text "\ \ \x. b[x]"}} \] \[ - \infer[@{text "(\\intro)"}]{@{text "\ - A \ A \ B"}}{@{text "\ \ B"}} + \infer[@{text "(\\intro)"}]{@{text "\ - A \ A \ B"}}{@{text "\ \ B"}} \qquad - \infer[@{text "(\\elim)"}]{@{text "\\<^sub>1 \ \\<^sub>2 \ B"}}{@{text "\\<^sub>1 \ A \ B"} & @{text "\\<^sub>2 \ A"}} + \infer[@{text "(\\elim)"}]{@{text "\\<^sub>1 \ \\<^sub>2 \ B"}}{@{text "\\<^sub>1 \ A \ B"} & @{text "\\<^sub>2 \ A"}} \] \caption{Primitive inferences of Pure}\label{fig:prim-rules} \end{center} @@ -554,7 +554,7 @@ \cite{Berghofer-Nipkow:2000:TPHOL}). Observe that locally fixed parameters (as in @{text - "\\intro"}) need not be recorded in the hypotheses, because + "\\intro"}) need not be recorded in the hypotheses, because the simple syntactic types of Pure are always inhabitable. ``Assumptions'' @{text "x :: \"} for type-membership are only present as long as some @{text "x\<^isub>\"} occurs in the statement diff -r 390de893659a -r d34154b08579 doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/ML.thy Tue May 03 22:28:19 2011 +0200 @@ -667,7 +667,7 @@ ML is augmented by special syntactic entities of the following form: @{rail " - @{syntax_def antiquote}: '@' '{' nameref args '}' | '\' | '\' + @{syntax_def antiquote}: '@{' nameref args '}' | '\' | '\' "} Here @{syntax nameref} and @{syntax args} are regular outer syntax diff -r 390de893659a -r d34154b08579 doc-src/IsarImplementation/Thy/Proof.thy --- a/doc-src/IsarImplementation/Thy/Proof.thy Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/Proof.thy Tue May 03 22:28:19 2011 +0200 @@ -253,14 +253,14 @@ \medskip The most basic export rule discharges assumptions directly by means of the @{text "\"} introduction rule: \[ - \infer[(@{text "\\intro"})]{@{text "\ - A \ A \ B"}}{@{text "\ \ B"}} + \infer[(@{text "\\intro"})]{@{text "\ - A \ A \ B"}}{@{text "\ \ B"}} \] The variant for goal refinements marks the newly introduced premises, which causes the canonical Isar goal refinement scheme to enforce unification with local premises within the goal: \[ - \infer[(@{text "#\\intro"})]{@{text "\ - A \ #A \ B"}}{@{text "\ \ B"}} + \infer[(@{text "#\\intro"})]{@{text "\ - A \ #A \ B"}}{@{text "\ \ B"}} \] \medskip Alternative versions of assumptions may perform arbitrary @@ -269,7 +269,7 @@ definition works by fixing @{text "x"} and assuming @{text "x \ t"}, with the following export rule to reverse the effect: \[ - \infer[(@{text "\\expand"})]{@{text "\ - (x \ t) \ B t"}}{@{text "\ \ B x"}} + \infer[(@{text "\\expand"})]{@{text "\ - (x \ t) \ B t"}}{@{text "\ \ B x"}} \] This works, because the assumption @{text "x \ t"} was introduced in a context with @{text "x"} being fresh, so @{text "x"} does not @@ -307,7 +307,7 @@ \item @{ML Assumption.add_assumes}~@{text "As"} is a special case of @{ML Assumption.add_assms} where the export rule performs @{text - "\\intro"} or @{text "#\\intro"}, depending on goal + "\\intro"} or @{text "#\\intro"}, depending on goal mode. \item @{ML Assumption.export}~@{text "is_goal inner outer thm"} diff -r 390de893659a -r d34154b08579 doc-src/IsarImplementation/Thy/document/Logic.tex --- a/doc-src/IsarImplementation/Thy/document/Logic.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Tue May 03 22:28:19 2011 +0200 @@ -217,15 +217,15 @@ \end{matharray} \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{ML antiquotation.class}{\mbox{\isa{class}}}}[] \rail@nont{\isa{nameref}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{ML antiquotation.sort}{\mbox{\isa{sort}}}}[] \rail@nont{\isa{sort}}[] \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@term{\hyperlink{ML antiquotation.type-name}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}name}}}}[] \rail@nextbar{1} @@ -235,7 +235,7 @@ \rail@endbar \rail@nont{\isa{nameref}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{ML antiquotation.typ}{\mbox{\isa{typ}}}}[] \rail@nont{\isa{type}}[] \rail@end @@ -481,7 +481,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{ML antiquotation.const-name}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}name}}}}[] \rail@nextbar{1} @@ -489,7 +489,7 @@ \rail@endbar \rail@nont{\isa{nameref}}[] \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{ML antiquotation.const}{\mbox{\isa{const}}}}[] \rail@bar \rail@nextbar{1} @@ -502,11 +502,11 @@ \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] \rail@endbar \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{ML antiquotation.term}{\mbox{\isa{term}}}}[] \rail@nont{\isa{term}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{ML antiquotation.prop}{\mbox{\isa{prop}}}}[] \rail@nont{\isa{prop}}[] \rail@end @@ -592,14 +592,14 @@ \infer[\isa{{\isaliteral{28}{\isacharparenleft}}assume{\isaliteral{29}{\isacharparenright}}}]{\isa{A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}{} \] \[ - \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} & \isa{x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}} + \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} & \isa{x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}} \qquad - \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C646173683E}{\isasymdash}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}} + \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}} \] \[ - \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}} + \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}} \qquad - \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} & \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}} + \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} & \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}} \] \caption{Primitive inferences of Pure}\label{fig:prim-rules} \end{center} @@ -626,7 +626,7 @@ terms, and \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} for proofs (cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}). - Observe that locally fixed parameters (as in \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro}) need not be recorded in the hypotheses, because + Observe that locally fixed parameters (as in \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro}) need not be recorded in the hypotheses, because the simple syntactic types of Pure are always inhabitable. ``Assumptions'' \isa{x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} for type-membership are only present as long as some \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} occurs in the statement @@ -813,27 +813,27 @@ \end{matharray} \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{ML antiquotation.ctyp}{\mbox{\isa{ctyp}}}}[] \rail@nont{\isa{typ}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{ML antiquotation.cterm}{\mbox{\isa{cterm}}}}[] \rail@nont{\isa{term}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{ML antiquotation.cprop}{\mbox{\isa{cprop}}}}[] \rail@nont{\isa{prop}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{ML antiquotation.thm}{\mbox{\isa{thm}}}}[] \rail@nont{\isa{thmref}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{ML antiquotation.thms}{\mbox{\isa{thms}}}}[] \rail@nont{\isa{thmrefs}}[] \rail@end -\rail@begin{6}{\isa{}} +\rail@begin{6}{} \rail@term{\hyperlink{ML antiquotation.lemma}{\mbox{\isa{lemma}}}}[] \rail@bar \rail@nextbar{1} diff -r 390de893659a -r d34154b08579 doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue May 03 22:28:19 2011 +0200 @@ -799,8 +799,7 @@ \begin{railoutput} \rail@begin{3}{\indexdef{}{syntax}{antiquote}\hypertarget{syntax.antiquote}{\hyperlink{syntax.antiquote}{\mbox{\isa{antiquote}}}}} \rail@bar -\rail@term{\isa{{\isaliteral{40}{\isacharat}}}}[] -\rail@term{\isa{{\isaliteral{7B}{\isacharbraceleft}}}}[] +\rail@term{\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}}}[] \rail@nont{\isa{nameref}}[] \rail@nont{\isa{args}}[] \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[] @@ -849,7 +848,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{ML antiquotation.let}{\mbox{\isa{let}}}}[] \rail@plus \rail@plus @@ -863,7 +862,7 @@ \rail@cterm{\isa{\isakeyword{and}}}[] \rail@endplus \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{ML antiquotation.note}{\mbox{\isa{note}}}}[] \rail@plus \rail@bar diff -r 390de893659a -r d34154b08579 doc-src/IsarImplementation/Thy/document/Prelim.tex --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Tue May 03 22:28:19 2011 +0200 @@ -265,7 +265,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}}[] \rail@bar \rail@nextbar{1} @@ -1721,7 +1721,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}}[] \rail@nont{\isa{name}}[] \rail@end diff -r 390de893659a -r d34154b08579 doc-src/IsarImplementation/Thy/document/Proof.tex --- a/doc-src/IsarImplementation/Thy/document/Proof.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Tue May 03 22:28:19 2011 +0200 @@ -397,14 +397,14 @@ \medskip The most basic export rule discharges assumptions directly by means of the \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} introduction rule: \[ - \infer[(\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}} + \infer[(\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}} \] The variant for goal refinements marks the newly introduced premises, which causes the canonical Isar goal refinement scheme to enforce unification with local premises within the goal: \[ - \infer[(\isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}} + \infer[(\isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}} \] \medskip Alternative versions of assumptions may perform arbitrary @@ -413,7 +413,7 @@ definition works by fixing \isa{x} and assuming \isa{x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t}, with the following export rule to reverse the effect: \[ - \infer[(\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{5C3C646173683E}{\isasymdash}}expand})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ t}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ x}} + \infer[(\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}expand})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ t}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ x}} \] This works, because the assumption \isa{x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} was introduced in a context with \isa{x} being fresh, so \isa{x} does not @@ -455,7 +455,7 @@ \verb|Assumption.assume|. \item \verb|Assumption.add_assumes|~\isa{As} is a special case of - \verb|Assumption.add_assms| where the export rule performs \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro} or \isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro}, depending on goal + \verb|Assumption.add_assms| where the export rule performs \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro} or \isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro}, depending on goal mode. \item \verb|Assumption.export|~\isa{is{\isaliteral{5F}{\isacharunderscore}}goal\ inner\ outer\ thm} diff -r 390de893659a -r d34154b08579 doc-src/IsarImplementation/Thy/document/Syntax.tex --- a/doc-src/IsarImplementation/Thy/document/Syntax.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex Tue May 03 22:28:19 2011 +0200 @@ -168,7 +168,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{4}{\isa{}} +\rail@begin{4}{} \rail@bar \rail@term{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[] \rail@nextbar{1} diff -r 390de893659a -r d34154b08579 doc-src/IsarImplementation/style.sty --- a/doc-src/IsarImplementation/style.sty Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarImplementation/style.sty Tue May 03 22:28:19 2011 +0200 @@ -64,15 +64,8 @@ \newcommand{\isasymTHEOREM}{\isakeyword{theorem}} \newcommand{\isasymDEFINITION}{\isakeyword{definition}} -\isabellestyle{it} -\newcommand{\isasymdash}{\mbox{-}} +\isabellestyle{itunderscore} -\underscoreon -\newcommand{\setupunderscore}{\def\isacharunderscore{\_}\def\isacharunderscorekeyword{\_}} -\setupunderscore - -\makeatletter -\def\rail@termfont{\isabellestyle{tt}\setupunderscore} -\def\rail@nontfont{\isabellestyle{it}\setupunderscore} -\def\rail@namefont{\isabellestyle{it}\setupunderscore} -\makeatother +\railtermfont{\isabellestyle{tt}} +\railnontermfont{\isabellestyle{itunderscore}} +\railnamefont{\isabellestyle{itunderscore}} diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/Document_Preparation.thy --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Tue May 03 22:28:19 2011 +0200 @@ -341,16 +341,16 @@ \item @{antiquotation_option_def show_abbrevs}~@{text "= bool"} controls folding of abbreviations. - \item @{antiquotation_option_def long_names}~@{text "= bool"} forces + \item @{antiquotation_option_def names_long}~@{text "= bool"} forces names of types and constants etc.\ to be printed in their fully qualified internal form. - \item @{antiquotation_option_def short_names}~@{text "= bool"} + \item @{antiquotation_option_def names_short}~@{text "= bool"} forces names of types and constants etc.\ to be printed unqualified. Note that internalizing the output again in the current context may well yield a different result. - \item @{antiquotation_option_def unique_names}~@{text "= bool"} + \item @{antiquotation_option_def names_unique}~@{text "= bool"} determines whether the printed version of qualified names should be made sufficiently long to avoid overlap with names declared further back. Set to @{text false} for more concise output. diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/Framework.thy --- a/doc-src/IsarRef/Thy/Framework.thy Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/Framework.thy Tue May 03 22:28:19 2011 +0200 @@ -424,7 +424,7 @@ \infer[(@{inference refinement})] {@{text "(\\<^vec>x. \<^vec>H \<^vec>x \ \<^vec>G' (\<^vec>a \<^vec>x))\ \ C\"}} {\begin{tabular}{rl} - @{text "sub\proof:"} & + @{text "sub\proof:"} & @{text "\<^vec>G \<^vec>a \ B \<^vec>a"} \\ @{text "goal:"} & @{text "(\\<^vec>x. \<^vec>H \<^vec>x \ B' \<^vec>x) \ C"} \\ @@ -436,7 +436,7 @@ \end{tabular}} \] - \noindent Here the @{text "sub\proof"} rule stems from the + \noindent Here the @{text "sub\proof"} rule stems from the main @{command fix}-@{command assume}-@{command show} outline of Isar (cf.\ \secref{sec:framework-subproof}): each assumption indicated in the text results in a marked premise @{text "G"} above. @@ -466,7 +466,7 @@ \medskip \begin{tabular}{rcl} - @{text "theory\stmt"} & = & @{command "theorem"}~@{text "statement proof |"}~~@{command "definition"}~@{text "\ | \"} \\[1ex] + @{text "theory\stmt"} & = & @{command "theorem"}~@{text "statement proof |"}~~@{command "definition"}~@{text "\ | \"} \\[1ex] @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\[1ex] @@ -582,7 +582,7 @@ \medskip \begin{tabular}{rcl} - @{command presume}~@{text A} & @{text "\"} & @{command assume}~@{text "\weak\discharge\ A"} \\ + @{command presume}~@{text A} & @{text "\"} & @{command assume}~@{text "\weak\discharge\ A"} \\ @{command def}~@{text "x \ a"} & @{text "\"} & @{command fix}~@{text x}~@{command assume}~@{text "\expansion\ x \ a"} \\ \end{tabular} \medskip @@ -591,14 +591,14 @@ \infer[(@{inference_def discharge})]{@{text "\\ - A \ #A \ B"}}{@{text "\\ \ B"}} \] \[ - \infer[(@{inference_def "weak\discharge"})]{@{text "\\ - A \ A \ B"}}{@{text "\\ \ B"}} + \infer[(@{inference_def "weak\discharge"})]{@{text "\\ - A \ A \ B"}}{@{text "\\ \ B"}} \] \[ \infer[(@{inference_def expansion})]{@{text "\\ - (x \ a) \ B a"}}{@{text "\\ \ B x"}} \] \medskip Note that @{inference discharge} and @{inference - "weak\discharge"} differ in the marker for @{prop A}, which is + "weak\discharge"} differ in the marker for @{prop A}, which is relevant when the result of a @{command fix}-@{command assume}-@{command show} outline is composed with a pending goal, cf.\ \secref{sec:framework-subproof}. diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue May 03 22:28:19 2011 +0200 @@ -100,9 +100,9 @@ @{attribute_def show_consts} & : & @{text attribute} & default @{text false} \\ @{attribute_def show_abbrevs} & : & @{text attribute} & default @{text true} \\ @{attribute_def show_brackets} & : & @{text attribute} & default @{text false} \\ - @{attribute_def long_names} & : & @{text attribute} & default @{text false} \\ - @{attribute_def short_names} & : & @{text attribute} & default @{text false} \\ - @{attribute_def unique_names} & : & @{text attribute} & default @{text true} \\ + @{attribute_def names_long} & : & @{text attribute} & default @{text false} \\ + @{attribute_def names_short} & : & @{text attribute} & default @{text false} \\ + @{attribute_def names_unique} & : & @{text attribute} & default @{text true} \\ @{attribute_def eta_contract} & : & @{text attribute} & default @{text true} \\ @{attribute_def goals_limit} & : & @{text attribute} & default @{text 10} \\ @{attribute_def show_main_goal} & : & @{text attribute} & default @{text false} \\ @@ -144,8 +144,8 @@ pretty printed entities may occasionally help to diagnose problems with operator priorities, for example. - \item @{attribute long_names}, @{attribute short_names}, and - @{attribute unique_names} control the way of printing fully + \item @{attribute names_long}, @{attribute names_short}, and + @{attribute names_unique} control the way of printing fully qualified internal names in external form. See also \secref{sec:antiq} for the document antiquotation options of the same names. diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/Quick_Reference.thy --- a/doc-src/IsarRef/Thy/Quick_Reference.thy Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/Quick_Reference.thy Tue May 03 22:28:19 2011 +0200 @@ -29,7 +29,7 @@ \begin{tabular}{rcl} @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\ - & @{text "|"} & @{text "prfx\<^sup>*"}~@{command "done"} \\[0.5ex] + & @{text "|"} & @{text "prfx\<^sup>*"}~@{command "done"} \\ @{text prfx} & = & @{command "apply"}~@{text method} \\ & @{text "|"} & @{command "using"}~@{text "facts"} \\ & @{text "|"} & @{command "unfolding"}~@{text "facts"} \\ @@ -58,7 +58,7 @@ @{command "hence"} & @{text "\"} & @{command "then"}~@{command "have"} \\ @{command "thus"} & @{text "\"} & @{command "then"}~@{command "show"} \\ @{command "from"}~@{text a} & @{text "\"} & @{command "note"}~@{text a}~@{command "then"} \\ - @{command "with"}~@{text a} & @{text "\"} & @{command "from"}~@{text "a \ this"} \\[0.5ex] + @{command "with"}~@{text a} & @{text "\"} & @{command "from"}~@{text "a \ this"} \\ @{command "from"}~@{text this} & @{text "\"} & @{command "then"} \\ @{command "from"}~@{text this}~@{command "have"} & @{text "\"} & @{command "hence"} \\ @{command "from"}~@{text this}~@{command "show"} & @{text "\"} & @{command "thus"} \\ @@ -141,7 +141,7 @@ text {* \begin{tabular}{ll} - \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex] + \multicolumn{2}{l}{\textbf{Rules}} \\[0.5ex] @{attribute OF}~@{text a} & rule resolved with facts (skipping ``@{text _}'') \\ @{attribute of}~@{text t} & rule instantiated with terms (skipping ``@{text _}'') \\ @{attribute "where"}~@{text "x = t"} & rule instantiated with terms, by variable name \\ diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/document/Document_Preparation.tex --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Tue May 03 22:28:19 2011 +0200 @@ -103,7 +103,7 @@ syntax. \begin{railoutput} -\rail@begin{5}{\isa{}} +\rail@begin{5}{} \rail@bar \rail@term{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}}[] \rail@nextbar{1} @@ -121,7 +121,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[] \rail@end -\rail@begin{7}{\isa{}} +\rail@begin{7}{} \rail@bar \rail@term{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}}[] \rail@nextbar{1} @@ -230,7 +230,7 @@ context. \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}}}[] \rail@nont{\isa{antiquotation}}[] \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[] @@ -497,16 +497,16 @@ \item \indexdef{}{antiquotation option}{show\_abbrevs}\hypertarget{antiquotation option.show-abbrevs}{\hyperlink{antiquotation option.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} controls folding of abbreviations. - \item \indexdef{}{antiquotation option}{long\_names}\hypertarget{antiquotation option.long-names}{\hyperlink{antiquotation option.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} forces + \item \indexdef{}{antiquotation option}{names\_long}\hypertarget{antiquotation option.names-long}{\hyperlink{antiquotation option.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} forces names of types and constants etc.\ to be printed in their fully qualified internal form. - \item \indexdef{}{antiquotation option}{short\_names}\hypertarget{antiquotation option.short-names}{\hyperlink{antiquotation option.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} + \item \indexdef{}{antiquotation option}{names\_short}\hypertarget{antiquotation option.names-short}{\hyperlink{antiquotation option.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} forces names of types and constants etc.\ to be printed unqualified. Note that internalizing the output again in the current context may well yield a different result. - \item \indexdef{}{antiquotation option}{unique\_names}\hypertarget{antiquotation option.unique-names}{\hyperlink{antiquotation option.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} + \item \indexdef{}{antiquotation option}{names\_unique}\hypertarget{antiquotation option.names-unique}{\hyperlink{antiquotation option.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} determines whether the printed version of qualified names should be made sufficiently long to avoid overlap with names declared further back. Set to \isa{false} for more concise output. @@ -642,7 +642,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\isa{rail}}[] \rail@nont{\isa{string}}[] \rail@end @@ -658,7 +658,7 @@ The rail specification language is quoted here as Isabelle \hyperlink{syntax.string}{\mbox{\isa{string}}}; it has its own grammar given below. \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@plus \rail@bar \rail@nextbar{1} @@ -750,7 +750,7 @@ \item Empty \verb|()| \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@end \end{railoutput} @@ -758,7 +758,7 @@ \item Nonterminal \verb|A| \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@nont{\isa{A}}[] \rail@end \end{railoutput} @@ -768,7 +768,7 @@ \verb|@{syntax method}| \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[] \rail@end \end{railoutput} @@ -777,7 +777,7 @@ \item Terminal \verb|'xyz'| \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\isa{xyz}}[] \rail@end \end{railoutput} @@ -786,7 +786,7 @@ \item Terminal in keyword style \verb|@'xyz'| \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\isa{\isakeyword{xyz}}}[] \rail@end \end{railoutput} @@ -796,7 +796,7 @@ \verb|@@{method rule}| \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[] \rail@end \end{railoutput} @@ -805,7 +805,7 @@ \item Concatenation \verb|A B C| \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@nont{\isa{A}}[] \rail@nont{\isa{B}}[] \rail@nont{\isa{C}}[] @@ -819,7 +819,7 @@ second one for escaping.} \verb|A B C \\ D E F| \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@nont{\isa{A}}[] \rail@nont{\isa{B}}[] \rail@nont{\isa{C}}[] @@ -834,7 +834,7 @@ \item Variants \verb|A |\verb,|,\verb| B |\verb,|,\verb| C| \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@nont{\isa{A}}[] \rail@nextbar{1} @@ -849,7 +849,7 @@ \item Option \verb|A ?| \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@nextbar{1} \rail@nont{\isa{A}}[] @@ -861,7 +861,7 @@ \item Repetition \verb|A *| \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@plus \rail@nextplus{1} \rail@cnont{\isa{A}}[] @@ -873,7 +873,7 @@ \item Repetition with separator \verb|A * sep| \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@nextbar{1} \rail@plus @@ -889,7 +889,7 @@ \item Strict repetition \verb|A +| \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@plus \rail@nont{\isa{A}}[] \rail@nextplus{1} @@ -901,7 +901,7 @@ \item Strict repetition with separator \verb|A + sep| \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@plus \rail@nont{\isa{A}}[] \rail@nextplus{1} @@ -926,7 +926,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isaliteral{5F}{\isacharunderscore}}drafts}}}}}[] \rail@nextbar{1} diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/document/Framework.tex --- a/doc-src/IsarRef/Thy/document/Framework.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Framework.tex Tue May 03 22:28:19 2011 +0200 @@ -538,7 +538,7 @@ \infer[(\hyperlink{inference.refinement}{\mbox{\isa{refinement}}})] {\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec G{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}{\isaliteral{22}{\isachardoublequote}}}} {\begin{tabular}{rl} - \isa{{\isaliteral{22}{\isachardoublequote}}sub{\isaliteral{5C3C646173683E}{\isasymdash}}proof{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & + \isa{{\isaliteral{22}{\isachardoublequote}}sub{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}proof{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec G\ \isaliteral{5C3C5E7665633E}{}\isactrlvec a\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ \isaliteral{5C3C5E7665633E}{}\isactrlvec a{\isaliteral{22}{\isachardoublequote}}} \\ \isa{{\isaliteral{22}{\isachardoublequote}}goal{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{27}{\isacharprime}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequote}}} \\ @@ -550,7 +550,7 @@ \end{tabular}} \] - \noindent Here the \isa{{\isaliteral{22}{\isachardoublequote}}sub{\isaliteral{5C3C646173683E}{\isasymdash}}proof{\isaliteral{22}{\isachardoublequote}}} rule stems from the + \noindent Here the \isa{{\isaliteral{22}{\isachardoublequote}}sub{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}proof{\isaliteral{22}{\isachardoublequote}}} rule stems from the main \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}-\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}-\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} outline of Isar (cf.\ \secref{sec:framework-subproof}): each assumption indicated in the text results in a marked premise \isa{{\isaliteral{22}{\isachardoublequote}}G{\isaliteral{22}{\isachardoublequote}}} above. @@ -580,7 +580,7 @@ \medskip \begin{tabular}{rcl} - \isa{{\isaliteral{22}{\isachardoublequote}}theory{\isaliteral{5C3C646173683E}{\isasymdash}}stmt{\isaliteral{22}{\isachardoublequote}}} & = & \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}statement\ proof\ \ {\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}~~\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex] + \isa{{\isaliteral{22}{\isachardoublequote}}theory{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}stmt{\isaliteral{22}{\isachardoublequote}}} & = & \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}statement\ proof\ \ {\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}~~\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex] \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{22}{\isachardoublequote}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}prfx\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}\ stmt\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex] @@ -687,7 +687,7 @@ \medskip \begin{tabular}{rcl} - \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}~\isa{A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6775696C6C656D6F746C6566743E}{\isasymguillemotleft}}weak{\isaliteral{5C3C646173683E}{\isasymdash}}discharge{\isaliteral{5C3C6775696C6C656D6F7472696768743E}{\isasymguillemotright}}\ A{\isaliteral{22}{\isachardoublequote}}} \\ + \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}~\isa{A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6775696C6C656D6F746C6566743E}{\isasymguillemotleft}}weak{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}discharge{\isaliteral{5C3C6775696C6C656D6F7472696768743E}{\isasymguillemotright}}\ A{\isaliteral{22}{\isachardoublequote}}} \\ \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ a{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6775696C6C656D6F746C6566743E}{\isasymguillemotleft}}expansion{\isaliteral{5C3C6775696C6C656D6F7472696768743E}{\isasymguillemotright}}\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ a{\isaliteral{22}{\isachardoublequote}}} \\ \end{tabular} \medskip @@ -696,13 +696,13 @@ \infer[(\indexdef{}{inference}{discharge}\hypertarget{inference.discharge}{\hyperlink{inference.discharge}{\mbox{\isa{discharge}}}})]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{22}{\isachardoublequote}}}} \] \[ - \infer[(\indexdef{}{inference}{weak-discharge}\hypertarget{inference.weak-discharge}{\hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isaliteral{5C3C646173683E}{\isasymdash}}discharge}}}})]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{22}{\isachardoublequote}}}} + \infer[(\indexdef{}{inference}{weak-discharge}\hypertarget{inference.weak-discharge}{\hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}discharge}}}})]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{22}{\isachardoublequote}}}} \] \[ \infer[(\indexdef{}{inference}{expansion}\hypertarget{inference.expansion}{\hyperlink{inference.expansion}{\mbox{\isa{expansion}}}})]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ a{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ x{\isaliteral{22}{\isachardoublequote}}}} \] - \medskip Note that \hyperlink{inference.discharge}{\mbox{\isa{discharge}}} and \hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isaliteral{5C3C646173683E}{\isasymdash}}discharge}}} differ in the marker for \isa{A}, which is + \medskip Note that \hyperlink{inference.discharge}{\mbox{\isa{discharge}}} and \hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}discharge}}} differ in the marker for \isa{A}, which is relevant when the result of a \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}-\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}-\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} outline is composed with a pending goal, cf.\ \secref{sec:framework-subproof}. diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/document/Generic.tex --- a/doc-src/IsarRef/Thy/document/Generic.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Tue May 03 22:28:19 2011 +0200 @@ -72,7 +72,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{6}{\isa{}} +\rail@begin{6}{} \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@bar \rail@nextbar{1} @@ -128,7 +128,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@term{\hyperlink{method.fold}{\mbox{\isa{fold}}}}[] \rail@nextbar{1} @@ -138,7 +138,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@term{\hyperlink{method.erule}{\mbox{\isa{erule}}}}[] \rail@nextbar{1} @@ -206,16 +206,16 @@ \end{matharray} \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}}[] \rail@nextbar{1} @@ -229,7 +229,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}}[] \rail@nextbar{1} @@ -237,7 +237,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}}[] \rail@bar \rail@nextbar{1} @@ -297,7 +297,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{method.subst}{\mbox{\isa{subst}}}}[] \rail@bar \rail@nextbar{1} @@ -316,7 +316,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.split}{\mbox{\isa{split}}}}[] \rail@bar \rail@nextbar{1} @@ -426,7 +426,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{6}{\isa{}} +\rail@begin{6}{} \rail@bar \rail@term{\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[] \rail@nextbar{1} @@ -452,7 +452,7 @@ \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}}[] \rail@bar \rail@nextbar{1} @@ -463,7 +463,7 @@ \rail@nextplus{1} \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isaliteral{5F}{\isacharunderscore}}tac}}}}[] \rail@bar \rail@nextbar{1} @@ -474,7 +474,7 @@ \rail@nextplus{1} \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isaliteral{5F}{\isacharunderscore}}tac}}}}[] \rail@bar \rail@nextbar{1} @@ -485,7 +485,7 @@ \rail@nont{\hyperlink{syntax.int}{\mbox{\isa{int}}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{method.tactic}{\mbox{\isa{tactic}}}}[] \rail@nextbar{1} @@ -570,7 +570,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{method.simp}{\mbox{\isa{simp}}}}[] \rail@nextbar{1} @@ -693,7 +693,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@term{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}}[] \rail@nextbar{1} @@ -738,7 +738,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{6}{\isa{}} +\rail@begin{6}{} \rail@term{\hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] @@ -760,7 +760,7 @@ \rail@endplus \rail@endbar \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{attribute.simproc}{\mbox{\isa{simproc}}}}[] \rail@bar \rail@bar @@ -818,7 +818,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}}[] \rail@bar \rail@nextbar{1} @@ -877,7 +877,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[] \rail@nextbar{1} @@ -936,7 +936,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.blast}{\mbox{\isa{blast}}}}[] \rail@bar \rail@nextbar{1} @@ -947,7 +947,7 @@ \rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[] \rail@endplus \rail@end -\rail@begin{5}{\isa{}} +\rail@begin{5}{} \rail@bar \rail@term{\hyperlink{method.fast}{\mbox{\isa{fast}}}}[] \rail@nextbar{1} @@ -1022,7 +1022,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.auto}{\mbox{\isa{auto}}}}[] \rail@bar \rail@nextbar{1} @@ -1034,7 +1034,7 @@ \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[] \rail@endplus \rail@end -\rail@begin{5}{\isa{}} +\rail@begin{5}{} \rail@bar \rail@term{\hyperlink{method.force}{\mbox{\isa{force}}}}[] \rail@nextbar{1} @@ -1146,7 +1146,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[] \rail@nextbar{1} @@ -1165,11 +1165,11 @@ \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] \rail@endbar \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[] \rail@term{\isa{del}}[] \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}}[] \rail@bar \rail@bar @@ -1272,11 +1272,11 @@ declarations internally. \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}}[] \rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}}[] \rail@bar \rail@nextbar{1} @@ -1285,7 +1285,7 @@ \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}}}[] \rail@bar \rail@nextbar{1} diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/document/HOLCF_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex Tue May 03 22:28:19 2011 +0200 @@ -55,7 +55,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOLCF.domain}{\mbox{\isa{\isacommand{domain}}}}}[] \rail@bar \rail@nextbar{1} diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue May 03 22:28:19 2011 +0200 @@ -32,7 +32,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[] \rail@bar \rail@nextbar{1} @@ -123,7 +123,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[] \rail@bar \rail@nextbar{1} @@ -237,7 +237,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[] \rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[] \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[] @@ -410,7 +410,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[] \rail@plus \rail@nont{\isa{dtspec}}[] @@ -418,7 +418,7 @@ \rail@cterm{\isa{\isakeyword{and}}}[] \rail@endplus \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[] \rail@bar \rail@nextbar{1} @@ -499,7 +499,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[] \rail@bar \rail@nextbar{1} @@ -552,7 +552,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[] \rail@bar \rail@nextbar{1} @@ -562,7 +562,7 @@ \rail@term{\isa{\isakeyword{where}}}[] \rail@nont{\isa{equations}}[] \rail@end -\rail@begin{4}{\isa{}} +\rail@begin{4}{} \rail@bar \rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[] \rail@nextbar{1} @@ -605,7 +605,7 @@ \rail@endplus \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[] \rail@bar \rail@nextbar{1} @@ -696,18 +696,18 @@ \end{matharray} \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[] \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[] \rail@plus \rail@nextplus{1} \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[] \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[] \rail@nont{\isa{orders}}[] \rail@plus @@ -781,7 +781,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{5}{\isa{}} +\rail@begin{5}{} \rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[] \rail@bar \rail@nextbar{1} @@ -866,7 +866,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{5}{\isa{}} +\rail@begin{5}{} \rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[] \rail@bar \rail@nextbar{1} @@ -886,7 +886,7 @@ \rail@nont{\isa{hints}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@nont{\isa{recdeftc}}[] \rail@bar \rail@nextbar{1} @@ -968,7 +968,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[] \rail@nextbar{1} @@ -1023,7 +1023,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{7}{\isa{}} +\rail@begin{7}{} \rail@bar \rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[] \rail@nextbar{1} @@ -1066,7 +1066,7 @@ \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[] \rail@endplus \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[] \rail@bar \rail@nextbar{1} @@ -1210,7 +1210,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}}[] \rail@plus \rail@nextplus{1} @@ -1246,7 +1246,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}}[] \rail@bar \rail@nextbar{1} @@ -1281,7 +1281,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{6}{\isa{}} +\rail@begin{6}{} \rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[] \rail@bar \rail@nextbar{1} @@ -1305,7 +1305,7 @@ \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}[] \rail@bar \rail@nextbar{1} @@ -1322,7 +1322,7 @@ \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}}[] \rail@bar \rail@nextbar{1} @@ -1407,7 +1407,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}[] \rail@bar \rail@nextbar{1} @@ -1421,7 +1421,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@term{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}[] \rail@nextbar{1} @@ -1440,7 +1440,7 @@ \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] \rail@endbar \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@term{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}}[] \rail@nextbar{1} @@ -1599,7 +1599,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[] \rail@bar \rail@nextbar{1} @@ -1611,7 +1611,7 @@ \rail@nont{\isa{rule}}[] \rail@endbar \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[] \rail@bar \rail@nextbar{1} @@ -1630,7 +1630,7 @@ \rail@nont{\isa{rule}}[] \rail@endbar \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] @@ -1645,7 +1645,7 @@ \rail@endplus \rail@endbar \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[] \rail@plus \rail@bar @@ -1751,7 +1751,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{11}{\isa{}} +\rail@begin{11}{} \rail@term{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}[] \rail@plus \rail@nont{\isa{constexpr}}[] @@ -1817,7 +1817,7 @@ \rail@term{\isa{Scala}}[] \rail@endbar \rail@end -\rail@begin{4}{\isa{}} +\rail@begin{4}{} \rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[] \rail@bar \rail@nextbar{1} @@ -1830,35 +1830,35 @@ \rail@endbar \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}}[] \rail@plus \rail@nont{\isa{const}}[] \rail@nextplus{1} \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[] \rail@plus \rail@nont{\isa{const}}[] \rail@nextplus{1} \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}}[] \rail@bar \rail@nextbar{1} \rail@term{\isa{del}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}}[] \rail@bar \rail@nextbar{1} \rail@term{\isa{del}}[] \rail@endbar \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[] \rail@bar \rail@nextbar{1} @@ -1868,7 +1868,7 @@ \rail@endplus \rail@endbar \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[] \rail@bar \rail@nextbar{1} @@ -1878,7 +1878,7 @@ \rail@endplus \rail@endbar \rail@end -\rail@begin{7}{\isa{}} +\rail@begin{7}{} \rail@term{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}}[] \rail@plus \rail@nont{\isa{const}}[] @@ -1901,7 +1901,7 @@ \rail@nextplus{6} \rail@endplus \rail@end -\rail@begin{7}{\isa{}} +\rail@begin{7}{} \rail@term{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}}}[] \rail@plus \rail@nont{\isa{typeconstructor}}[] @@ -1924,7 +1924,7 @@ \rail@nextplus{6} \rail@endplus \rail@end -\rail@begin{9}{\isa{}} +\rail@begin{9}{} \rail@term{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}}[] \rail@plus \rail@nont{\isa{class}}[] @@ -1948,7 +1948,7 @@ \rail@nextplus{8} \rail@endplus \rail@end -\rail@begin{7}{\isa{}} +\rail@begin{7}{} \rail@term{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}}[] \rail@plus \rail@nont{\isa{typeconstructor}}[] @@ -1973,7 +1973,7 @@ \rail@nextplus{6} \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}}[] \rail@nont{\isa{target}}[] \rail@plus @@ -1981,13 +1981,13 @@ \rail@nextplus{1} \rail@endplus \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}}[] \rail@nont{\isa{const}}[] \rail@nont{\isa{const}}[] \rail@nont{\isa{target}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}}[] \rail@nont{\isa{target}}[] \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[] @@ -1997,7 +1997,7 @@ \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}}[] \rail@nont{\isa{target}}[] \rail@plus @@ -2006,7 +2006,7 @@ \rail@nextplus{1} \rail@endplus \rail@end -\rail@begin{11}{\isa{}} +\rail@begin{11}{} \rail@term{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}}[] \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[] \rail@cr{2} @@ -2189,7 +2189,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{11}{\isa{}} +\rail@begin{11}{} \rail@bar \rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[] \rail@nextbar{1} @@ -2241,7 +2241,7 @@ \rail@endplus \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}}[] \rail@plus \rail@nont{\isa{codespec}}[] @@ -2256,7 +2256,7 @@ \rail@nont{\isa{attachment}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}}[] \rail@plus \rail@nont{\isa{tycodespec}}[] @@ -2289,7 +2289,7 @@ \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[] \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[] \rail@bar \rail@nextbar{1} @@ -2565,7 +2565,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{6}{\isa{}} +\rail@begin{6}{} \rail@bar \rail@term{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}}[] \rail@nextbar{1} diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 22:28:19 2011 +0200 @@ -45,7 +45,7 @@ internal logical entities in a human-readable fashion. \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}[] \rail@bar \rail@nextbar{1} @@ -53,7 +53,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}[] \rail@bar \rail@nextbar{1} @@ -61,7 +61,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}[] \rail@bar \rail@nextbar{1} @@ -69,7 +69,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}[] \rail@bar \rail@nextbar{1} @@ -77,7 +77,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}[] \rail@nextbar{1} @@ -92,7 +92,7 @@ \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}[] \rail@bar \rail@nextbar{1} @@ -175,9 +175,9 @@ \indexdef{}{attribute}{show\_consts}\hypertarget{attribute.show-consts}{\hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}}} & : & \isa{attribute} & default \isa{false} \\ \indexdef{}{attribute}{show\_abbrevs}\hypertarget{attribute.show-abbrevs}{\hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}} & : & \isa{attribute} & default \isa{true} \\ \indexdef{}{attribute}{show\_brackets}\hypertarget{attribute.show-brackets}{\hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}}} & : & \isa{attribute} & default \isa{false} \\ - \indexdef{}{attribute}{long\_names}\hypertarget{attribute.long-names}{\hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\ - \indexdef{}{attribute}{short\_names}\hypertarget{attribute.short-names}{\hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\ - \indexdef{}{attribute}{unique\_names}\hypertarget{attribute.unique-names}{\hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{true} \\ + \indexdef{}{attribute}{names\_long}\hypertarget{attribute.names-long}{\hyperlink{attribute.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}} & : & \isa{attribute} & default \isa{false} \\ + \indexdef{}{attribute}{names\_short}\hypertarget{attribute.names-short}{\hyperlink{attribute.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}} & : & \isa{attribute} & default \isa{false} \\ + \indexdef{}{attribute}{names\_unique}\hypertarget{attribute.names-unique}{\hyperlink{attribute.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}}} & : & \isa{attribute} & default \isa{true} \\ \indexdef{}{attribute}{eta\_contract}\hypertarget{attribute.eta-contract}{\hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}}} & : & \isa{attribute} & default \isa{true} \\ \indexdef{}{attribute}{goals\_limit}\hypertarget{attribute.goals-limit}{\hyperlink{attribute.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}{\isadigit{0}}} \\ \indexdef{}{attribute}{show\_main\_goal}\hypertarget{attribute.show-main-goal}{\hyperlink{attribute.show-main-goal}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal}}}} & : & \isa{attribute} & default \isa{false} \\ @@ -219,8 +219,8 @@ pretty printed entities may occasionally help to diagnose problems with operator priorities, for example. - \item \hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}, \hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}, and - \hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}} control the way of printing fully + \item \hyperlink{attribute.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}, \hyperlink{attribute.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}, and + \hyperlink{attribute.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}} control the way of printing fully qualified internal names in external form. See also \secref{sec:antiq} for the document antiquotation options of the same names. @@ -488,7 +488,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{5}{\isa{}} +\rail@begin{5}{} \rail@bar \rail@term{\hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}notation}}}}}[] \rail@nextbar{1} @@ -510,7 +510,7 @@ \rail@cterm{\isa{\isakeyword{and}}}[] \rail@endplus \rail@end -\rail@begin{5}{\isa{}} +\rail@begin{5}{} \rail@bar \rail@term{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}}[] \rail@nextbar{1} @@ -532,7 +532,7 @@ \rail@cterm{\isa{\isakeyword{and}}}[] \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}}[] \rail@bar \rail@nextbar{1} @@ -899,7 +899,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] @@ -907,7 +907,7 @@ \rail@cterm{\isa{\isakeyword{and}}}[] \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}}[] \rail@nextbar{1} @@ -922,7 +922,7 @@ \rail@nextplus{1} \rail@endplus \rail@end -\rail@begin{7}{\isa{}} +\rail@begin{7}{} \rail@bar \rail@term{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}}[] \rail@nextbar{1} @@ -1017,7 +1017,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{5}{\isa{}} +\rail@begin{5}{} \rail@bar \rail@term{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[] \rail@nextbar{1} diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/document/Misc.tex --- a/doc-src/IsarRef/Thy/document/Misc.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Misc.tex Tue May 03 22:28:19 2011 +0200 @@ -42,7 +42,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}}}[] \rail@nextbar{1} @@ -53,7 +53,7 @@ \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[] \rail@endbar \rail@end -\rail@begin{6}{\isa{}} +\rail@begin{6}{} \rail@term{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}[] \rail@bar \rail@nextbar{1} @@ -99,7 +99,7 @@ \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}}[] \rail@plus \rail@nextplus{1} @@ -123,11 +123,11 @@ \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[] \rail@endbar \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[] \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[] \rail@bar \rail@nextbar{1} @@ -259,7 +259,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}[] \rail@nextbar{1} diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/document/Proof.tex --- a/doc-src/IsarRef/Thy/document/Proof.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Tue May 03 22:28:19 2011 +0200 @@ -75,11 +75,11 @@ \end{matharray} \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}}[] \rail@term{\isa{\isakeyword{begin}}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}}[] \rail@end \end{railoutput} @@ -220,7 +220,7 @@ exporting some result \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} yields \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}t{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}. \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[] @@ -228,7 +228,7 @@ \rail@cterm{\isa{\isakeyword{and}}}[] \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}}[] \rail@nextbar{1} @@ -240,7 +240,7 @@ \rail@cterm{\isa{\isakeyword{and}}}[] \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}}[] \rail@plus \rail@nont{\isa{def}}[] @@ -331,7 +331,7 @@ input process just after type checking. Also note that \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} does not support polymorphism. \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}}[] \rail@plus \rail@plus @@ -403,7 +403,7 @@ issuing a follow-up claim. \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}}[] \rail@plus \rail@bar @@ -415,7 +415,7 @@ \rail@cterm{\isa{\isakeyword{and}}}[] \rail@endplus \rail@end -\rail@begin{4}{\isa{}} +\rail@begin{4}{} \rail@bar \rail@term{\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}}[] \rail@nextbar{1} @@ -538,7 +538,7 @@ and assumptions, cf.\ \secref{sec:obtain}). \begin{railoutput} -\rail@begin{6}{\isa{}} +\rail@begin{6}{} \rail@bar \rail@term{\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}}[] \rail@nextbar{1} @@ -562,7 +562,7 @@ \rail@nont{\isa{longgoal}}[] \rail@endbar \rail@end -\rail@begin{4}{\isa{}} +\rail@begin{4}{} \rail@bar \rail@term{\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}}[] \rail@nextbar{1} @@ -574,7 +574,7 @@ \rail@endbar \rail@nont{\isa{goal}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}}}}}[] \rail@bar \rail@nextbar{1} @@ -849,21 +849,21 @@ assumption in the very last step. \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}}[] \rail@bar \rail@nextbar{1} \rail@nont{\isa{method}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}}[] \rail@bar \rail@nextbar{1} \rail@nont{\isa{method}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}}[] \rail@nont{\isa{method}}[] \rail@bar @@ -871,7 +871,7 @@ \rail@nont{\isa{method}}[] \rail@endbar \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@term{\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}}[] \rail@nextbar{1} @@ -954,14 +954,14 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.fact}{\mbox{\isa{fact}}}}[] \rail@bar \rail@nextbar{1} \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}}[] \rail@bar \rail@nextbar{1} @@ -993,7 +993,7 @@ \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[] \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[] \rail@nextbar{1} @@ -1012,15 +1012,15 @@ \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] \rail@endbar \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}}[] \rail@term{\isa{del}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}}[] \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{attribute.of}{\mbox{\isa{of}}}}[] \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[] \rail@bar @@ -1030,7 +1030,7 @@ \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[] \rail@endbar \rail@end -\rail@begin{6}{\isa{}} +\rail@begin{6}{} \rail@term{\hyperlink{attribute.where}{\mbox{\isa{where}}}}[] \rail@bar \rail@nextbar{1} @@ -1160,7 +1160,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}}[] \rail@nextbar{1} @@ -1168,14 +1168,14 @@ \rail@endbar \rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}}[] \rail@bar \rail@nextbar{1} \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] \rail@endbar \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}}[] \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] \rail@end @@ -1234,7 +1234,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[] @@ -1309,7 +1309,7 @@ occur in the conclusion. \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}}[] \rail@bar \rail@nextbar{1} @@ -1327,7 +1327,7 @@ \rail@cterm{\isa{\isakeyword{and}}}[] \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[] @@ -1441,7 +1441,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}}[] \rail@nextbar{1} @@ -1454,7 +1454,7 @@ \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] \rail@endbar \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{attribute.trans}{\mbox{\isa{trans}}}}[] \rail@bar \rail@nextbar{1} @@ -1566,7 +1566,7 @@ later. \begin{railoutput} -\rail@begin{4}{\isa{}} +\rail@begin{4}{} \rail@term{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}}[] \rail@bar \rail@nont{\isa{caseref}}[] @@ -1591,14 +1591,14 @@ \rail@nont{\isa{attributes}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@nextplus{1} \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@plus @@ -1606,7 +1606,7 @@ \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@endplus \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{attribute.params}{\mbox{\isa{params}}}}[] \rail@plus \rail@plus @@ -1617,7 +1617,7 @@ \rail@cterm{\isa{\isakeyword{and}}}[] \rail@endplus \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}}[] \rail@bar \rail@nextbar{1} @@ -1700,7 +1700,7 @@ ``strengthened'' inductive statements within the object-logic. \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[] \rail@bar \rail@nextbar{1} @@ -1721,7 +1721,7 @@ \rail@nont{\isa{rule}}[] \rail@endbar \rail@end -\rail@begin{6}{\isa{}} +\rail@begin{6}{} \rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[] \rail@bar \rail@nextbar{1} @@ -1751,7 +1751,7 @@ \rail@nont{\isa{rule}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[] \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[] \rail@nont{\isa{taking}}[] @@ -1987,15 +1987,15 @@ \end{matharray} \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}}[] \rail@nont{\isa{spec}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}}[] \rail@nont{\isa{spec}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}}[] \rail@nont{\isa{spec}}[] \rail@end diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/document/Quick_Reference.tex --- a/doc-src/IsarRef/Thy/document/Quick_Reference.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex Tue May 03 22:28:19 2011 +0200 @@ -51,7 +51,7 @@ \begin{tabular}{rcl} \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{22}{\isachardoublequote}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}prfx\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}\ stmt\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}} \\ - & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}prfx\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} \\[0.5ex] + & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}prfx\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} \\ \isa{prfx} & = & \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{method} \\ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}facts{\isaliteral{22}{\isachardoublequote}}} \\ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}facts{\isaliteral{22}{\isachardoublequote}}} \\ @@ -82,7 +82,7 @@ \hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} \\ \hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} \\ \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{a} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{a}~\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} \\ - \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}~\isa{a} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ this{\isaliteral{22}{\isachardoublequote}}} \\[0.5ex] + \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}~\isa{a} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ this{\isaliteral{22}{\isachardoublequote}}} \\ \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} \\ \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}} \\ \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}} \\ @@ -173,7 +173,7 @@ % \begin{isamarkuptext}% \begin{tabular}{ll} - \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex] + \multicolumn{2}{l}{\textbf{Rules}} \\[0.5ex] \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{a} & rule resolved with facts (skipping ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'') \\ \hyperlink{attribute.of}{\mbox{\isa{of}}}~\isa{t} & rule instantiated with terms (skipping ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'') \\ \hyperlink{attribute.where}{\mbox{\isa{where}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} & rule instantiated with terms, by variable name \\ diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Tue May 03 22:28:19 2011 +0200 @@ -69,7 +69,7 @@ admissible. \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@term{\isa{\isakeyword{imports}}}[] @@ -145,7 +145,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@term{\isa{\isakeyword{begin}}}[] @@ -220,7 +220,7 @@ available, and result names need not be given. \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}}[] \rail@bar \rail@nextbar{1} @@ -232,7 +232,7 @@ \rail@nont{\isa{specs}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}[] \rail@bar \rail@nextbar{1} @@ -249,7 +249,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}}[] \rail@bar \rail@nextbar{1} @@ -383,7 +383,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}}[] \rail@nextbar{1} @@ -401,7 +401,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}}[] \rail@bar \rail@nextbar{1} @@ -568,7 +568,7 @@ \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} \indexisarelem{defines}\indexisarelem{notes} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@bar @@ -581,7 +581,7 @@ \rail@term{\isa{\isakeyword{begin}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locale}}}}}[] \rail@bar \rail@nextbar{1} @@ -783,7 +783,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}}[] \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[] \rail@bar @@ -791,7 +791,7 @@ \rail@nont{\isa{equations}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}}[] \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[] \rail@bar @@ -799,7 +799,7 @@ \rail@nont{\isa{equations}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}}[] \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] \rail@bar @@ -813,7 +813,7 @@ \rail@nont{\isa{equations}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}}[] \rail@bar \rail@nextbar{1} @@ -821,7 +821,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}[] \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] \rail@end @@ -965,7 +965,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{8}{\isa{}} +\rail@begin{8}{} \rail@term{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[] @@ -990,7 +990,7 @@ \rail@term{\isa{\isakeyword{begin}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] @@ -1001,10 +1001,10 @@ \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[] \rail@term{\isa{\isakeyword{begin}}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] @@ -1014,7 +1014,7 @@ \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[] \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}}[] \rail@bar \rail@nextbar{1} @@ -1022,7 +1022,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[] \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] \rail@bar @@ -1032,10 +1032,10 @@ \rail@endbar \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[] \rail@end \end{railoutput} @@ -1197,7 +1197,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{5}{\isa{}} +\rail@begin{5}{} \rail@term{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}}[] \rail@cr{2} \rail@plus @@ -1259,11 +1259,11 @@ \end{matharray} \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@end -\rail@begin{6}{\isa{}} +\rail@begin{6}{} \rail@bar \rail@term{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}}[] \rail@nextbar{1} @@ -1279,7 +1279,7 @@ \rail@endbar \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[] \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[] @@ -1383,14 +1383,14 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.classdecl}{\mbox{\isa{classdecl}}}}[] \rail@nextplus{1} \rail@endplus \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] @@ -1404,7 +1404,7 @@ \rail@cterm{\isa{\isakeyword{and}}}[] \rail@endplus \rail@end -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isaliteral{5F}{\isacharunderscore}}sort}}}}}[] \rail@nont{\hyperlink{syntax.sort}{\mbox{\isa{sort}}}}[] \rail@end @@ -1453,7 +1453,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}}[] \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[] \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[] @@ -1463,7 +1463,7 @@ \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}}[] \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[] \rail@bar @@ -1471,7 +1471,7 @@ \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[] \rail@endbar \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] @@ -1553,7 +1553,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] @@ -1566,7 +1566,7 @@ \rail@nextplus{2} \rail@endplus \rail@end -\rail@begin{6}{\isa{}} +\rail@begin{6}{} \rail@term{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}}[] \rail@bar \rail@nextbar{1} @@ -1626,7 +1626,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[] @@ -1634,7 +1634,7 @@ \rail@nextplus{1} \rail@endplus \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@bar \rail@term{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}}[] \rail@nextbar{1} @@ -1704,7 +1704,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{1}{\isa{}} +\rail@begin{1}{} \rail@term{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[] @@ -1743,7 +1743,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{4}{\isa{}} +\rail@begin{4}{} \rail@bar \rail@nont{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}class}}}}}[] \rail@nextbar{1} diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/Thy/document/ZF_Specific.tex --- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex Tue May 03 22:28:19 2011 +0200 @@ -40,7 +40,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}}[] \rail@bar \rail@nextbar{1} @@ -88,7 +88,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{command.ZF.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[] \rail@nextbar{1} @@ -163,7 +163,7 @@ In the following syntax specification \isa{{\isaliteral{22}{\isachardoublequote}}monos{\isaliteral{22}{\isachardoublequote}}}, \isa{typeintros}, and \isa{typeelims} are the same as above. \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{command.ZF.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[] \rail@nextbar{1} @@ -243,7 +243,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[] \rail@plus \rail@bar @@ -274,7 +274,7 @@ \end{matharray} \begin{railoutput} -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@bar \rail@term{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[] \rail@nextbar{1} @@ -286,14 +286,14 @@ \rail@endbar \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@end -\rail@begin{2}{\isa{}} +\rail@begin{2}{} \rail@term{\hyperlink{method.ZF.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[] \rail@plus \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] \rail@nextplus{1} \rail@endplus \rail@end -\rail@begin{3}{\isa{}} +\rail@begin{3}{} \rail@term{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[] \rail@plus \rail@bar diff -r 390de893659a -r d34154b08579 doc-src/IsarRef/style.sty --- a/doc-src/IsarRef/style.sty Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/IsarRef/style.sty Tue May 03 22:28:19 2011 +0200 @@ -36,15 +36,8 @@ \parindent 0pt\parskip 0.5ex -\isabellestyle{it} -\newcommand{\isasymdash}{\mbox{-}} +\isabellestyle{itunderscore} -\underscoreon -\newcommand{\setupunderscore}{\def\isacharunderscore{\_}\def\isacharunderscorekeyword{\_}} -\setupunderscore - -\makeatletter -\def\rail@termfont{\isabellestyle{tt}\setupunderscore} -\def\rail@nontfont{\isabellestyle{it}\setupunderscore} -\def\rail@namefont{\isabellestyle{it}\setupunderscore} -\makeatother +\railtermfont{\isabellestyle{tt}} +\railnontermfont{\isabellestyle{itunderscore}} +\railnamefont{\isabellestyle{itunderscore}} diff -r 390de893659a -r d34154b08579 doc-src/LaTeXsugar/Sugar/Sugar.thy --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Tue May 03 22:28:19 2011 +0200 @@ -152,7 +152,7 @@ the qualified name, for example @{text "T.length"}, where @{text T} is the theory it is defined in, to distinguish it from the predefined @{const[source] "List.length"}. In case there is no danger of confusion, you can insist on -short names (no qualifiers) by setting the \verb!short_names! +short names (no qualifiers) by setting the \verb!names_short! configuration option in the context. *} diff -r 390de893659a -r d34154b08579 doc-src/LaTeXsugar/Sugar/document/Sugar.tex --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Tue May 03 22:28:19 2011 +0200 @@ -195,7 +195,7 @@ If there are multiple declarations of the same name, Isabelle prints the qualified name, for example \isa{T{\isaliteral{2E}{\isachardot}}length}, where \isa{T} is the theory it is defined in, to distinguish it from the predefined \isa{{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}length{\isaliteral{22}{\isachardoublequote}}}. In case there is no danger of confusion, you can insist on -short names (no qualifiers) by setting the \verb!short_names! +short names (no qualifiers) by setting the \verb!names_short! configuration option in the context.% \end{isamarkuptext}% \isamarkuptrue% diff -r 390de893659a -r d34154b08579 doc-src/System/system.tex --- a/doc-src/System/system.tex Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/System/system.tex Tue May 03 22:28:19 2011 +0200 @@ -4,6 +4,7 @@ \usepackage{../iman,../extra,../isar,../ttbox} \usepackage[nohyphen,strings]{../underscore} \usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym} +\usepackage{../../lib/texinputs/railsetup} \usepackage{../IsarRef/style} \usepackage{../pdfsetup} diff -r 390de893659a -r d34154b08579 doc-src/TutorialI/Misc/Itrev.thy --- a/doc-src/TutorialI/Misc/Itrev.thy Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/TutorialI/Misc/Itrev.thy Tue May 03 22:28:19 2011 +0200 @@ -2,7 +2,7 @@ theory Itrev imports Main begin -declare [[unique_names = false]] +declare [[names_unique = false]] (*>*) section{*Induction Heuristics*} @@ -141,6 +141,6 @@ \index{induction heuristics|)} *} (*<*) -declare [[unique_names = true]] +declare [[names_unique = true]] end (*>*) diff -r 390de893659a -r d34154b08579 doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Tue May 03 21:46:49 2011 +0200 +++ b/doc-src/antiquote_setup.ML Tue May 03 22:28:19 2011 +0200 @@ -19,7 +19,7 @@ | "{" => "\\{" | "|" => "$\\mid$" | "}" => "\\}" - | "\" => "-" + | "\" => "-" | c => c); fun clean_name "\" = "dots" @@ -28,7 +28,7 @@ | clean_name "_" = "underscore" | clean_name "{" = "braceleft" | clean_name "}" = "braceright" - | clean_name s = s |> translate (fn "_" => "-" | "\" => "-" | c => c); + | clean_name s = s |> translate (fn "_" => "-" | "\" => "-" | c => c); (* verbatim text *) diff -r 390de893659a -r d34154b08579 lib/texinputs/isabelle.sty --- a/lib/texinputs/isabelle.sty Tue May 03 21:46:49 2011 +0200 +++ b/lib/texinputs/isabelle.sty Tue May 03 22:28:19 2011 +0200 @@ -186,6 +186,14 @@ \def\isacharverbatimclose{\isamath{\rangle\!\rangle}}% } +\newcommand{\isabellestyleitunderscore}{% +%requires underscore.sty +\underscoreon% +\isabellestyleit% +\def\isacharunderscore{\_}% +\def\isacharunderscorekeyword{\_}% +} + \newcommand{\isabellestylesl}{% \isabellestyleit% \def\isastyle{\small\sl}% diff -r 390de893659a -r d34154b08579 lib/texinputs/railsetup.sty --- a/lib/texinputs/railsetup.sty Tue May 03 21:46:49 2011 +0200 +++ b/lib/texinputs/railsetup.sty Tue May 03 22:28:19 2011 +0200 @@ -1195,7 +1195,7 @@ % default setup for Isabelle \newenvironment{railoutput}% -{\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\end{list}} +{\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\makeatother\end{list}} \def\rail@termfont{\isabellestyle{tt}} \def\rail@nontfont{\isabellestyle{it}} diff -r 390de893659a -r d34154b08579 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Tue May 03 21:46:49 2011 +0200 +++ b/src/Pure/General/name_space.ML Tue May 03 22:28:19 2011 +0200 @@ -20,15 +20,15 @@ val markup: T -> string -> Markup.T val is_concealed: T -> string -> bool val intern: T -> xstring -> string - val long_names_default: bool Unsynchronized.ref - val long_names_raw: Config.raw - val long_names: bool Config.T - val short_names_default: bool Unsynchronized.ref - val short_names_raw: Config.raw - val short_names: bool Config.T - val unique_names_default: bool Unsynchronized.ref - val unique_names_raw: Config.raw - val unique_names: bool Config.T + val names_long_default: bool Unsynchronized.ref + val names_long_raw: Config.raw + val names_long: bool Config.T + val names_short_default: bool Unsynchronized.ref + val names_short_raw: Config.raw + val names_short: bool Config.T + val names_unique_default: bool Unsynchronized.ref + val names_unique_raw: Config.raw + val names_unique: bool Config.T val extern: Proof.context -> T -> string -> xstring val hide: bool -> string -> T -> T val merge: T * T -> T @@ -161,33 +161,33 @@ fun intern space xname = #1 (lookup space xname); -val long_names_default = Unsynchronized.ref false; -val long_names_raw = Config.declare "long_names" (fn _ => Config.Bool (! long_names_default)); -val long_names = Config.bool long_names_raw; +val names_long_default = Unsynchronized.ref false; +val names_long_raw = Config.declare "names_long" (fn _ => Config.Bool (! names_long_default)); +val names_long = Config.bool names_long_raw; -val short_names_default = Unsynchronized.ref false; -val short_names_raw = Config.declare "short_names" (fn _ => Config.Bool (! short_names_default)); -val short_names = Config.bool short_names_raw; +val names_short_default = Unsynchronized.ref false; +val names_short_raw = Config.declare "names_short" (fn _ => Config.Bool (! names_short_default)); +val names_short = Config.bool names_short_raw; -val unique_names_default = Unsynchronized.ref true; -val unique_names_raw = Config.declare "unique_names" (fn _ => Config.Bool (! unique_names_default)); -val unique_names = Config.bool unique_names_raw; +val names_unique_default = Unsynchronized.ref true; +val names_unique_raw = Config.declare "names_unique" (fn _ => Config.Bool (! names_unique_default)); +val names_unique = Config.bool names_unique_raw; fun extern ctxt space name = let - val long_names = Config.get ctxt long_names; - val short_names = Config.get ctxt short_names; - val unique_names = Config.get ctxt unique_names; + val names_long = Config.get ctxt names_long; + val names_short = Config.get ctxt names_short; + val names_unique = Config.get ctxt names_unique; fun valid require_unique xname = let val (name', is_unique) = lookup space xname in name = name' andalso (not require_unique orelse is_unique) end; fun ext [] = if valid false name then name else hidden name - | ext (nm :: nms) = if valid unique_names nm then nm else ext nms; + | ext (nm :: nms) = if valid names_unique nm then nm else ext nms; in - if long_names then name - else if short_names then Long_Name.base_name name + if names_long then name + else if names_short then Long_Name.base_name name else ext (get_accesses space name) end; diff -r 390de893659a -r d34154b08579 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue May 03 21:46:49 2011 +0200 +++ b/src/Pure/Isar/attrib.ML Tue May 03 22:28:19 2011 +0200 @@ -441,9 +441,9 @@ register_config Printer.show_question_marks_raw #> register_config Syntax.ambiguity_level_raw #> register_config Syntax_Trans.eta_contract_raw #> - register_config Name_Space.long_names_raw #> - register_config Name_Space.short_names_raw #> - register_config Name_Space.unique_names_raw #> + register_config Name_Space.names_long_raw #> + register_config Name_Space.names_short_raw #> + register_config Name_Space.names_unique_raw #> register_config ML_Context.trace_raw #> register_config Proof_Context.show_abbrevs_raw #> register_config Goal_Display.goals_limit_raw #> diff -r 390de893659a -r d34154b08579 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Tue May 03 21:46:49 2011 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Tue May 03 22:28:19 2011 +0200 @@ -124,7 +124,7 @@ bool_pref Goal_Display.show_consts_default "show-consts" "Show types of consts in Isabelle goal display", - bool_pref Name_Space.long_names_default + bool_pref Name_Space.names_long_default "long-names" "Show fully qualified names in Isabelle terms", bool_pref Printer.show_brackets_default diff -r 390de893659a -r d34154b08579 src/Pure/Thy/rail.ML --- a/src/Pure/Thy/rail.ML Tue May 03 21:46:49 2011 +0200 +++ b/src/Pure/Thy/rail.ML Tue May 03 22:28:19 2011 +0200 @@ -242,7 +242,8 @@ val (rail', y') = vertical_range rail 0; val out_name = (case name of - Antiquote.Text s => output_text false s + Antiquote.Text "" => "" + | Antiquote.Text s => output_text false s | Antiquote.Antiq a => output_antiq a); in "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^ diff -r 390de893659a -r d34154b08579 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Tue May 03 21:46:49 2011 +0200 +++ b/src/Pure/Thy/thy_output.ML Tue May 03 22:28:19 2011 +0200 @@ -450,9 +450,9 @@ val _ = add_option "show_structs" (Config.put show_structs o boolean); val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean); val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean); -val _ = add_option "long_names" (Config.put Name_Space.long_names o boolean); -val _ = add_option "short_names" (Config.put Name_Space.short_names o boolean); -val _ = add_option "unique_names" (Config.put Name_Space.unique_names o boolean); +val _ = add_option "names_long" (Config.put Name_Space.names_long o boolean); +val _ = add_option "names_short" (Config.put Name_Space.names_short o boolean); +val _ = add_option "names_unique" (Config.put Name_Space.names_unique o boolean); val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean); val _ = add_option "display" (Config.put display o boolean); val _ = add_option "break" (Config.put break o boolean); diff -r 390de893659a -r d34154b08579 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Tue May 03 21:46:49 2011 +0200 +++ b/src/Pure/Tools/find_theorems.ML Tue May 03 22:28:19 2011 +0200 @@ -383,9 +383,9 @@ val shorten = Name_Space.extern (ctxt - |> Config.put Name_Space.long_names false - |> Config.put Name_Space.short_names false - |> Config.put Name_Space.unique_names false) space; + |> Config.put Name_Space.names_long false + |> Config.put Name_Space.names_short false + |> Config.put Name_Space.names_unique false) space; fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = nicer_name (shorten x, i) (shorten y, j)