diff -r fdc3b5bcd79d -r 73f1c6685367 doc-src/Tutorial/IsaMakefile
--- a/doc-src/Tutorial/IsaMakefile	Fri Aug 04 10:59:28 2000 +0200
+++ b/doc-src/Tutorial/IsaMakefile	Fri Aug 04 11:22:59 2000 +0200
@@ -5,6 +5,9 @@
 ## targets
 
 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Datatype HOL-Recdef HOL-Misc
+images:
+test:
+all: default
 
 
 ## global settings