doc-src/ProgProve/Thys/document/Bool_nat_list.tex

 \begin{isamarkuptext}%
 yields \isa{Cons\ b\ {\isaliteral{28}{\isacharparenleft}}Cons\ a\ Nil{\isaliteral{29}{\isacharparenright}}}.
 \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
 %left-hand side, but that on the right-hand side each of the argument
 %types of a constructor needs to be enclosed in quotation marks.