diff --git a/INSTALL b/INSTALL
index 2c2b0b6..e85a343 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,14 +1,17 @@
 Installation
 ============
 
-IsarMathLib is an Isabelle 2005 session. 
+IsarMathLib is an Isabelle session.
 Isabelle is a theorem proving environment developed at Cambridge University and TU Munich (see http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html).
-Isabelle needs to be installed on the machine before you can generate IsarMathLib proof documents or verify the proofs. 
-The installation method described in the INSTALL file of Isabelle 2005 worked fine on my Debian system. If you have Debian proofgeneral package installed from Debian repositories, I suggest to remove (purge) it before installing Isabelle. Isabelle package contains Proof General (an authoring tool for theory files) that is well set up to work with Isabelle. As IsarMathLib uses ZF logics, you need to download and install  ZF_*.tar.gz file for your platform from the Isabelle site. 
+Isabelle needs to be installed on the machine before you can generate IsarMathLib proof documents or verify the proofs. Isabelle 2005 or later should work.
+
+The installation method described in the INSTALL file of Isabelle 2005 worked fine on my Debian system. If you have Debian proofgeneral package installed from Debian repositories, I suggest to remove (purge) it before installing Isabelle. Isabelle package contains Proof General (an authoring tool for theory files) that is well set up to work with Isabelle. You also need to install the ZF logic which is distributed with Isabelle. Do this by going to the directory where you have unpacked Isabelle and typing "./build ZF".
 
 You may also try the unofficial Debian packages from Achim D. Brucker (http://www.brucker.ch/projects/debian/).
 
-After unpacking the IsarMathLib project the theory files can be processed with the "isatool make" issued in the main project directory (where the IsaMakefile is).
+After unpacking the IsarMathLib project, make sure you have latex (including extras, for example in Debian run "apt-get install texlive-latex-extras".
+
+Then process the theory files with the "isabelle make" command issued in the main project directory (where the IsaMakefile is). (For older versions of Isabelle, "isatool make"). This will take a while, but will eventually create a few PDF files (and tell you the names of the files). You can also type "isabelle" to see what your other choices are (for example, "isabelle jedit" or "isabelle emacs").
 
 If you wish to browse/modify theory files with Proof General, set your logic to ZF (Isabelle/Isar/Logics/ZF).