doc-src/LaTeXsugar/Sugar/Sugar.thy
changeset 24496 65f3b37f80b7
parent 22834 bf67f798f063
child 24497 7840f760a744
     1.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Aug 30 22:35:40 2007 +0200
     1.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Aug 31 12:24:00 2007 +0200
     1.3 @@ -133,6 +133,19 @@
     1.4  
     1.5  (*<*)ML"reset show_question_marks"(*>*)
     1.6  
     1.7 +subsection {*Qualified names*}
     1.8 +
     1.9 +text{* If there are multiple declarations of the same name, Isabelle prints
    1.10 +the qualified name, for example @{text "T.length"}, where @{text T} is the
    1.11 +theory it is defined in, to distinguish it from the predefined @{const[source]
    1.12 +"List.length"}. In case there is no danger of confusion, you can insist on
    1.13 +short names (no qualifiers) by setting \verb!short_names!, typically
    1.14 +in \texttt{ROOT.ML}:
    1.15 +\begin{verbatim}
    1.16 +set short_names;
    1.17 +\end{verbatim}
    1.18 +*}
    1.19 +
    1.20  subsection {*Variable names\label{sec:varnames}*}
    1.21  
    1.22  text{* It sometimes happens that you want to change the name of a