diff -r db8e302f44c8 -r d5accbc67e1b ProgTutorial/document/root.tex
--- a/ProgTutorial/document/root.tex	Thu Mar 26 19:00:51 2009 +0000
+++ b/ProgTutorial/document/root.tex	Fri Mar 27 12:49:28 2009 +0000
@@ -43,6 +43,7 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \hyphenation{Isabelle}
 \renewcommand{\isasymiota}{}
+\renewcommand{\isamarkupsubsection}[1]{\subsection*{#1}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % to work around a problem with \isanewline