Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
tuned text, improved dependencies
authornipkow
Wed, 18 Apr 2012 18:24:16 +0200
changeset 484122d49b0c9d8ec
parent 48411 a2850a16e30f
child 48413 1a5dc8377b5c
tuned text, improved dependencies
doc-src/ProgProve/Makefile file | annotate | diff | comparison | revisions
doc-src/ProgProve/intro-isabelle.tex file | annotate | diff | comparison | revisions 
     1.1 --- a/doc-src/ProgProve/Makefile	Wed Apr 18 17:04:03 2012 +0200
     1.2 +++ b/doc-src/ProgProve/Makefile	Wed Apr 18 18:24:16 2012 +0200
     1.3 @@ -9,8 +9,9 @@
     1.4  
     1.5  NAME = prog-prove
     1.6  
     1.7 -FILES = prog-prove.tex prog-prove.bib Thys/document/*.tex prelude.tex \
     1.8 -  svmono.cls mathpartir.sty isabelle.sty isabellesym.sty Thys/MyList.thy
     1.9 +FILES = prog-prove.tex prog-prove.bib intro-isabelle.tex \
    1.10 +  Thys/document/*.tex Thys/MyList.thy \
    1.11 +  prelude.tex svmono.cls mathpartir.sty isabelle.sty isabellesym.sty
    1.12  
    1.13  dvi: $(NAME).dvi
    1.14  

     2.1 --- a/doc-src/ProgProve/intro-isabelle.tex	Wed Apr 18 17:04:03 2012 +0200
     2.2 +++ b/doc-src/ProgProve/intro-isabelle.tex	Wed Apr 18 18:24:16 2012 +0200
     2.3 @@ -35,4 +35,13 @@
     2.4  For a comprehensive treatment of all things Isabelle we recommend the
     2.5  \emph{Isabelle/Isar Reference Manual}~\cite{IsarRef}, which comes with the
     2.6  Isabelle distribution.
     2.7 -The tutorial by Nipkow, Paulson and Wenzel~\cite{LNCS2283} (in its updated version that comes with the Isabelle distribution) is still recommended for the wealth of examples and material, but its proof style is outdated. In particular it fails to cover the structured proof language Isar.
     2.8 \ No newline at end of file
     2.9 +The tutorial by Nipkow, Paulson and Wenzel~\cite{LNCS2283} (in its updated version that comes with the Isabelle distribution) is still recommended for the wealth of examples and material, but its proof style is outdated. In particular it fails to cover the structured proof language Isar.
    2.10 +
    2.11 +This introduction has grown out of many years of teaching Isabelle courses.
    2.12 +It tries to cover the essentials (from a functional programming point of
    2.13 +view) as quickly and compactly as possible. There is also an accompanying
    2.14 +set of \LaTeX-based slides available from the author on request.
    2.15 +
    2.16 +\paragraph{Acknowledgements}
    2.17 +I wish to thank the following people for their comments on this text:
    2.18 +Florian Haftmann, Ren\'{e} Thiemann and Christian Sternagel.
    2.19 \ No newline at end of file
wneuper/isa