# HG changeset patch
# User nipkow
# Date 1335257044 -7200
# Node ID 8aac84627b849a37ee44bae7aeb9edb322471cea
# Parent  39229c76063684d8e679cba44870385e9f36fc74
the perennial doc problem of how to define lists a second time

diff -r 39229c760636 -r 8aac84627b84 doc-src/ProgProve/Thys/Bool_nat_list.thy
--- 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
diff -r 39229c760636 -r 8aac84627b84 doc-src/ProgProve/Thys/document/Bool_nat_list.tex
--- 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