# HG changeset patch # User nipkow # Date 1333390330 -7200 # Node ID 70239da25ef61ea31bf9d0bff50b688d5f4a32c0 # Parent 2511f3e8449628040b6e3bc41acb09765b001fd5 towards showing " in the tutorial diff -r 2511f3e84496 -r 70239da25ef6 doc-src/ProgProve/Thys/Basics.thy --- a/doc-src/ProgProve/Thys/Basics.thy Mon Apr 02 13:47:00 2012 +0200 +++ b/doc-src/ProgProve/Thys/Basics.thy Mon Apr 02 20:12:10 2012 +0200 @@ -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 diff -r 2511f3e84496 -r 70239da25ef6 doc-src/ProgProve/Thys/Bool_nat_list.thy --- a/doc-src/ProgProve/Thys/Bool_nat_list.thy Mon Apr 02 13:47:00 2012 +0200 +++ b/doc-src/ProgProve/Thys/Bool_nat_list.thy Mon Apr 02 20:12:10 2012 +0200 @@ -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 \ 'a list \ '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} diff -r 2511f3e84496 -r 70239da25ef6 doc-src/ProgProve/Thys/MyList.thy --- a/doc-src/ProgProve/Thys/MyList.thy Mon Apr 02 13:47:00 2012 +0200 +++ b/doc-src/ProgProve/Thys/MyList.thy Mon Apr 02 20:12:10 2012 +0200 @@ -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" | diff -r 2511f3e84496 -r 70239da25ef6 doc-src/ProgProve/Thys/document/Basics.tex --- a/doc-src/ProgProve/Thys/document/Basics.tex Mon Apr 02 13:47:00 2012 +0200 +++ b/doc-src/ProgProve/Thys/document/Basics.tex Mon Apr 02 20:12:10 2012 +0200 @@ -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% % diff -r 2511f3e84496 -r 70239da25ef6 doc-src/ProgProve/Thys/document/Bool_nat_list.tex --- a/doc-src/ProgProve/Thys/document/Bool_nat_list.tex Mon Apr 02 13:47:00 2012 +0200 +++ b/doc-src/ProgProve/Thys/document/Bool_nat_list.tex Mon Apr 02 20:12:10 2012 +0200 @@ -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} diff -r 2511f3e84496 -r 70239da25ef6 doc-src/ProgProve/prelude.tex --- a/doc-src/ProgProve/prelude.tex Mon Apr 02 13:47:00 2012 +0200 +++ b/doc-src/ProgProve/prelude.tex Mon Apr 02 20:12:10 2012 +0200 @@ -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}