--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 22:26:16 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 22:27:32 2011 +0200
@@ -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.