--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Aug 30 22:35:40 2007 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Aug 31 12:24:00 2007 +0200
@@ -133,6 +133,19 @@
(*<*)ML"reset show_question_marks"(*>*)
+subsection {*Qualified names*}
+
+text{* If there are multiple declarations of the same name, Isabelle prints
+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 \verb!short_names!, typically
+in \texttt{ROOT.ML}:
+\begin{verbatim}
+set short_names;
+\end{verbatim}
+*}
+
subsection {*Variable names\label{sec:varnames}*}
text{* It sometimes happens that you want to change the name of a
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Aug 30 22:35:40 2007 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Aug 31 12:24:00 2007 +0200
@@ -182,6 +182,22 @@
%
\endisadelimML
%
+\isamarkupsubsection{Qualified names%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+If there are multiple declarations of the same name, Isabelle prints
+the qualified name, for example \isa{T{\isachardot}length}, where \isa{T} is the
+theory it is defined in, to distinguish it from the predefined \isa{{\isachardoublequote}List{\isachardot}length{\isachardoublequote}}. In case there is no danger of confusion, you can insist on
+short names (no qualifiers) by setting \verb!short_names!, typically
+in \texttt{ROOT.ML}:
+\begin{verbatim}
+set short_names;
+\end{verbatim}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Variable names\label{sec:varnames}%
}
\isamarkuptrue%
@@ -461,7 +477,7 @@
Note the space between \verb!@! and \verb!{! in the tabular argument.
It prevents Isabelle from interpreting \verb!@ {~~...~~}!
as an antiquotation. The styles \verb!lhs! and \verb!rhs!
- extract the left hand side (or right hand side respectively) from the
+ extract the left hand side (or right hand side respectivly) from the
conclusion of propositions consisting of a binary operator
(e.~g.~\isa{{\isacharequal}}, \isa{{\isasymequiv}}, \isa{{\isacharless}}).
@@ -531,7 +547,7 @@
After this \verb!setup!,
there will be a new style available named \verb!my_concl!, thus allowing
- antiquotations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}!
+ antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}!
yielding \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}.%
\end{isamarkuptext}%
\isamarkuptrue%