--- a/ProgTutorial/Intro.thy	Thu May 23 00:58:11 2019 +0100
+++ b/ProgTutorial/Intro.thy	Tue Jun 11 23:31:09 2019 +0100
@@ -29,7 +29,7 @@
   The best way to get to know the Isabelle/ML is by experimenting
   with the many code examples included in the tutorial. The code is as far as
   possible checked against the Isabelle
-  distribution.%%\footnote{\input{version.tex}}
+  distribution. %%\footnote{\input{version.tex}}
   If something does not work, then
   please let us know. It is impossible for us to know every environment,
   operating system or editor in which Isabelle is used. If you have comments,
@@ -51,8 +51,13 @@
   based on jEdit. This part of the code is beyond the interest of this
   tutorial, since it mostly does not concern the regular Isabelle 
   developer.
+\<close>
 
-  The rich Isabelle infrastructure can be categorized by various aspects @{cite "wenzel-technology"}:
+section \<open>Isabelle Infrastructure\<close>
+
+text \<open>
+There is a rich Isabelle infrastructure---it might be good to have the  following
+rough mind map @{cite "wenzel-technology"}:
 
      @{emph \<open>@{bold \<open>Logic\<close>}\<close>} 
       \begin{description}

--- a/ProgTutorial/document/root.bib	Thu May 23 00:58:11 2019 +0100
+++ b/ProgTutorial/document/root.bib	Tue Jun 11 23:31:09 2019 +0100
@@ -1,21 +1,18 @@
 @Misc{Bornat-lecture,
   author =	 {R.~Bornat},
   title =	 {In {D}efence of {P}rogramming},
-  howpublished = {Available online via
-                  \url{http://www.cs.mdx.ac.uk/staffpages/r_bornat/lectures/ revisedinauguraltext.pdf}},
   month =	 {April},
   year =	 2005,
   note =	 {Corrected and revised version of inaugural lecture,
                   delivered on 22nd January 2004 at the School of
                   Computing Science, Middlesex University}
 }
-@Misc{wenzel-technology,
+@manual{wenzel-technology,
   author = {M.~Wenzel},
-  title = {Further Scaling of Isabelle Technology},
-  howpublished = {http://sketis.net},
+  title = {{F}urther {S}caling of {I}sabelle {T}echnology},
+  note = {\url{http://sketis.net}},
   month = {April},
-  year = {2018},
-  note = {},
+  year = {2018}
 }
 
 @Book{isa-tutorial,
@@ -23,20 +20,23 @@
   title		= {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
   publisher	= {Springer},
   year		= 2002,
-  note		= {LNCS Tutorial 2283}}
+  note		= {LNCS Tutorial 2283}
+}
 
 @book{paulson-ml2,
   author	= {Lawrence C. Paulson},
   title		= {{ML} for the Working Programmer},
   year		= 1996,
   edition	= {2nd},
-  publisher	= {Cambridge University Press}}
+  publisher	= {Cambridge University Press}
+}
 
 @manual{isa-imp,
   author	= {M.~Wenzel},
   title		= {The {Isabelle/Isar} Implementation},
   institution	= {Technische Universit\"at M\"unchen},
-  note          = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
+  note          = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}
+}
 
 
 @book{GordonMilnerWadsworth79,