--- a/doc-src/ProgProve/Thys/Basics.thy Mon Apr 02 21:26:07 2012 +0100
+++ b/doc-src/ProgProve/Thys/Basics.thy Mon Apr 02 21:26:46 2012 +0100
@@ -136,10 +136,13 @@
single identifier can be dropped. When Isabelle prints a syntax error
message, it refers to the HOL syntax as the \concept{inner syntax} and the
enclosing theory language as the \concept{outer syntax}.
+\sem
\begin{warn}
For reasons of readability, we almost never show the quotation marks in this
book. Consult the accompanying theory files to see where they need to go.
\end{warn}
+\endsem
+%
*}
(*<*)
end
--- a/doc-src/ProgProve/Thys/Bool_nat_list.thy Mon Apr 02 21:26:07 2012 +0100
+++ b/doc-src/ProgProve/Thys/Bool_nat_list.thy Mon Apr 02 21:26:46 2012 +0100
@@ -158,13 +158,19 @@
done
declare [[names_short]]
(*>*)
-datatype 'a list = Nil | Cons "'a" "('a list)"
+datatype 'a list = Nil | Cons 'a "'a list"
-text{* This means that all lists are built up from @{const Nil}, the empty
-list, and @{const Cons}, the operation of putting an element in front of a
-list. Hence all lists are of the form @{const Nil}, or @{term"Cons x Nil"},
+text{*
+\begin{itemize}
+\item Type @{typ "'a list"} is the type of list over elements of type @{typ 'a}. Because @{typ 'a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
+\item Lists have two constructors: @{const Nil}, the empty list, and @{const Cons}, which puts an element (of type @{typ 'a}) in front of a list (of type @{typ "'a list"}).
+Hence all lists are of the form @{const Nil}, or @{term"Cons x Nil"},
or @{term"Cons x (Cons y Nil)"} etc.
-
+\item \isacom{datatype} requires no quotation marks on the
+left-hand side, but on the right-hand side each of the argument
+types of a constructor needs to be enclosed in quotation marks, unless
+it is just an identifier (e.g.\ @{typ nat} or @{typ 'a}).
+\end{itemize}
We also define two standard functions, append and reverse: *}
fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -189,11 +195,12 @@
text{* yields @{value "rev(Cons a (Cons b Nil))"}.
\medskip
-Figure~\ref{fig:MyList} shows the theory created so far. 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.
+Figure~\ref{fig:MyList} shows the theory created so far.
+% 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.
\begin{figure}[htbp]
\begin{alltt}
--- a/doc-src/ProgProve/Thys/MyList.thy Mon Apr 02 21:26:07 2012 +0100
+++ b/doc-src/ProgProve/Thys/MyList.thy Mon Apr 02 21:26:46 2012 +0100
@@ -2,7 +2,7 @@
imports Main
begin
-datatype 'a list = Nil | Cons "'a" "('a list)"
+datatype 'a list = Nil | Cons 'a "'a list"
fun app :: "'a list => 'a list => 'a list" where
"app Nil ys = ys" |
--- a/doc-src/ProgProve/Thys/document/Basics.tex Mon Apr 02 21:26:07 2012 +0100
+++ b/doc-src/ProgProve/Thys/document/Basics.tex Mon Apr 02 21:26:46 2012 +0100
@@ -147,10 +147,13 @@
single identifier can be dropped. When Isabelle prints a syntax error
message, it refers to the HOL syntax as the \concept{inner syntax} and the
enclosing theory language as the \concept{outer syntax}.
+\sem
\begin{warn}
For reasons of readability, we almost never show the quotation marks in this
book. Consult the accompanying theory files to see where they need to go.
-\end{warn}%
+\end{warn}
+\endsem
+%%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/ProgProve/Thys/document/Bool_nat_list.tex Mon Apr 02 21:26:07 2012 +0100
+++ b/doc-src/ProgProve/Thys/document/Bool_nat_list.tex Mon Apr 02 21:26:46 2012 +0100
@@ -216,13 +216,18 @@
%
\endisadelimproof
\isacommand{datatype}\isamarkupfalse%
-\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{3D}{\isacharequal}}\ Nil\ {\isaliteral{7C}{\isacharbar}}\ Cons\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{3D}{\isacharequal}}\ Nil\ {\isaliteral{7C}{\isacharbar}}\ Cons\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
-This means that all lists are built up from \isa{Nil}, the empty
-list, and \isa{Cons}, the operation of putting an element in front of a
-list. Hence all lists are of the form \isa{Nil}, or \isa{Cons\ x\ Nil},
+\begin{itemize}
+\item Type \isa{{\isaliteral{27}{\isacharprime}}a\ list} is the type of list over elements of type \isa{{\isaliteral{27}{\isacharprime}}a}. Because \isa{{\isaliteral{27}{\isacharprime}}a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
+\item Lists have two constructors: \isa{Nil}, the empty list, and \isa{Cons}, which puts an element (of type \isa{{\isaliteral{27}{\isacharprime}}a}) in front of a list (of type \isa{{\isaliteral{27}{\isacharprime}}a\ list}).
+Hence all lists are of the form \isa{Nil}, or \isa{Cons\ x\ Nil},
or \isa{Cons\ x\ {\isaliteral{28}{\isacharparenleft}}Cons\ y\ Nil{\isaliteral{29}{\isacharparenright}}} etc.
-
+\item \isacom{datatype} requires no quotation marks on the
+left-hand side, but on the right-hand side each of the argument
+types of a constructor needs to be enclosed in quotation marks, unless
+it is just an identifier (e.g.\ \isa{nat} or \isa{{\isaliteral{27}{\isacharprime}}a}).
+\end{itemize}
We also define two standard functions, append and reverse:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -254,11 +259,12 @@
yields \isa{Cons\ b\ {\isaliteral{28}{\isacharparenleft}}Cons\ a\ Nil{\isaliteral{29}{\isacharparenright}}}.
\medskip
-Figure~\ref{fig:MyList} shows the theory created so far. 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.
+Figure~\ref{fig:MyList} shows the theory created so far.
+% 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.
\begin{figure}[htbp]
\begin{alltt}
--- a/doc-src/ProgProve/prelude.tex Mon Apr 02 21:26:07 2012 +0100
+++ b/doc-src/ProgProve/prelude.tex Mon Apr 02 21:26:46 2012 +0100
@@ -88,9 +88,9 @@
\hbox to0pt{\hskip-\hangindent\warnbang\hfill}\ignorespaces}
{\par\end{trivlist}}
-\renewcommand{\isachardoublequote}{}
-\renewcommand{\isachardoublequoteopen}{}
-\renewcommand{\isachardoublequoteclose}{}
+\chardef\isachardoublequote=`\"%
+\chardef\isachardoublequoteopen=`\"%
+\chardef\isachardoublequoteclose=`\"%
\renewcommand{\isacharbackquoteopen}{\isacharbackquote}
\renewcommand{\isacharbackquoteclose}{\isacharbackquote}