# HG changeset patch
# User nipkow
# Date 1188555840 -7200
# Node ID 65f3b37f80b7d53631b51f5b1e63d3f6c0f31233
# Parent  eab1b52a47d037c3393e3e3f248fddb773d1a66b
added short_names explanation

diff -r eab1b52a47d0 -r 65f3b37f80b7 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- 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
diff -r eab1b52a47d0 -r 65f3b37f80b7 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- 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%