--- a/doc-src/ProgProve/Thys/Bool_nat_list.thy Tue Apr 24 09:47:40 2012 +0200
+++ b/doc-src/ProgProve/Thys/Bool_nat_list.thy Tue Apr 24 10:44:04 2012 +0200
@@ -196,6 +196,12 @@
\medskip
Figure~\ref{fig:MyList} shows the theory created so far.
+Because @{text list}, @{const Nil}, @{const Cons} etc are already predefined,
+ Isabelle prints qualified (long) names when executing this theory, for example, @{text MyList.Nil}
+ instead of @{const Nil}.
+ To suppress the qualified names you can insert the command
+ \texttt{declare [[names\_short]]}.
+ This is not recommended in general but just for this unusual example.
% Notice where the
%quotations marks are needed that we mostly sweep under the carpet. In
%particular, notice that \isacom{datatype} requires no quotation marks on the
--- a/doc-src/ProgProve/Thys/document/Bool_nat_list.tex Tue Apr 24 09:47:40 2012 +0200
+++ b/doc-src/ProgProve/Thys/document/Bool_nat_list.tex Tue Apr 24 10:44:04 2012 +0200
@@ -260,6 +260,12 @@
\medskip
Figure~\ref{fig:MyList} shows the theory created so far.
+Because \isa{list}, \isa{Nil}, \isa{Cons} etc are already predefined,
+ Isabelle prints qualified (long) names when executing this theory, for example, \isa{MyList{\isaliteral{2E}{\isachardot}}Nil}
+ instead of \isa{Nil}.
+ To suppress the qualified names you can insert the command
+ \texttt{declare [[names\_short]]}.
+ This is not recommended in general but just for this unusual example.
% Notice where the
%quotations marks are needed that we mostly sweep under the carpet. In
%particular, notice that \isacom{datatype} requires no quotation marks on the