--- a/ProgTutorial/Package/Ind_Prelims.thy	Wed Apr 29 00:36:14 2009 +0200
+++ b/ProgTutorial/Package/Ind_Prelims.thy	Tue May 05 03:21:49 2009 +0200
@@ -1,5 +1,5 @@
 theory Ind_Prelims
-imports Main LaTeXsugar "../Base" 
+imports Main "../Base" 
 begin
 
 section{* Preliminaries *}
@@ -15,9 +15,7 @@
   we will figure out a general method for
   defining inductive predicates.  The aim in this section is \emph{not} to
   write proofs that are as beautiful as possible, but as close as possible to
-  the ML-code we will develop in later sections.
-
-
+  the ML-implementation we will develop in later sections.
 
   We first consider the transitive closure of a relation @{text R}. The 
   ``pencil-and-paper'' specification for the transitive closure is:
@@ -161,7 +159,7 @@
 
 text {*
   Now we are done. It might be surprising that we are not using the automatic
-  tactics available in Isabelle for proving this lemmas. After all @{text
+  tactics available in Isabelle/HOL for proving this lemmas. After all @{text
   "blast"} would easily dispense of it.
 *}