--- a/ProgTutorial/FirstSteps.thy	Sat May 30 17:40:20 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat May 30 23:58:05 2009 +0200
@@ -318,11 +318,11 @@
 text {* and typographically more economical than *}
 
 ML{*fun inc_by_five x =
-   let val y1 = x + 1
-       val y2 = (y1, y1)
-       val y3 = fst y2
-       val y4 = y3 + 4
-   in y4 end*}
+let val y1 = x + 1
+    val y2 = (y1, y1)
+    val y3 = fst y2
+    val y4 = y3 + 4
+in y4 end*}
 
 text {* 
   Another reason why the let-bindings in the code above are better to be
@@ -339,7 +339,7 @@
       |> map (pair "z")
       |> Variable.variant_frees ctxt [f]
       |> map Free  
-      |> (curry list_comb) f *}
+      |> curry list_comb f *}
 
 text {*
   This code extracts the argument types of a given function @{text "f"} and then generates 
@@ -1966,8 +1966,8 @@
 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 
 100016, 100017, 100018, 100019, 100020"}
 
-  where @{ML upto} generates a list of integers. You can print this
-  list out as an ``set'', that means enclosed inside @{text [quotes] "{"} and
+  where @{ML upto} generates a list of integers. You can print out this
+  list as an ``set'', that means enclosed inside @{text [quotes] "{"} and
   @{text [quotes] "}"}, and separated by commas using the function
   @{ML [index] enum in Pretty}. For example
 *}
@@ -1985,10 +1985,10 @@
   100016, 100017, 100018, 100019, 100020}"}
 
   As can be seen, this function prints out the ``set'' so that starting 
-  from the second each new line as an indentation of 2.
+  from the second, each new line as an indentation of 2.
   
-  If you print something out which goes beyond the capabilities of the
-  standard function, you can do realatively easily the formating
+  If you print out something that goes beyond the capabilities of the
+  standard functions, you can do realatively easily the formating
   yourself. Assume you want to print out a list of items where like in ``English''
   the last two items are separated by @{text [quotes] "and"}. For this you can
   write the function
@@ -2006,7 +2006,7 @@
       end *}
 
 text {*
-  where in Line 7 we print the beginning of the list and in Line
+  where Line 7 prints the beginning of the list and Line
   8 the last item. We have to use @{ML "Pretty.brk 1"} in order
   to insert a space (of length 1) before the 
   @{text [quotes] "and"}. This space is also a pleace where a linebreak 
@@ -2038,14 +2038,15 @@
 end*}
 
 text {*
-  In Line 3 we define a function that inserts according to spaces 
-  possible linebreaks into an (English). In Lines 4 and 5 we pretty-print
-  the term and its type using the functions @{ML [index] pretty_term in Syntax} and
-  @{ML [index] pretty_typ in Syntax}. We also use the function @{ML [index] quote in Pretty}
-  in order to enclose the term and type inside quotation marks. In Line 
-  9 we add a period right after the type without the possibility of a 
+  In Line 3 we define a function that inserts possible linebreaks in places
+  where a space is. In Lines 4 and 5 we pretty-print the term and its type
+  using the functions @{ML [index] pretty_term in Syntax} and @{ML [index]
+  pretty_typ in Syntax}. We also use the function @{ML [index] quote in
+  Pretty} in order to enclose the term and type inside quotation marks. In
+  Line 9 we add a period right after the type without the possibility of a
   linebreak, because we do not want that a linebreak occurs there.
 
+
   Now you can write
 
   @{ML_response_fake [display,gray]
@@ -2060,6 +2061,8 @@
   "The term \"op = (op = (op = (op = (op = op =))))\" has type 
 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
 
+
+  FIXME: TBD below
 *}
 
 ML {* pprint (Pretty.big_list "header"  (map (Pretty.str o string_of_int) (4 upto 10))) *}

--- a/ProgTutorial/document/root.tex	Sat May 30 17:40:20 2009 +0200
+++ b/ProgTutorial/document/root.tex	Sat May 30 23:58:05 2009 +0200
@@ -16,6 +16,7 @@
 \usepackage{mathpartir}
 \usepackage{flafter}
 \usepackage{makeidx}
+\usepackage{tocbibind}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
@@ -25,10 +26,6 @@
 \isadroptag{theory}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% adding chapters explicitly to the table of content
-\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % indexing
 \makeindex
 \newcommand{\indexdef}[2]{\index{#1 (#2)}}
@@ -161,20 +158,20 @@
 \maketitle
 
 % table of contents
-\tocentry{\contentsname}
+\frontmatter
 \setcounter{tocdepth}{1}
 \tableofcontents
 
 % generated text of all theories
+\mainmatter
 \input{session}
 
 % bibliography
-\tocentry{\bibname}
+\backmatter
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 % index
-\tocentry{\indexname}
 \printindex
 
 \end{document}

Binary file progtutorial.pdf has changed