diff -r 839340b78fc8 -r 1eb980d64ba3 Admin/makerpm
--- a/Admin/makerpm	Wed Sep 20 14:59:19 2000 +0200
+++ b/Admin/makerpm	Wed Sep 20 21:20:01 2000 +0200
@@ -7,7 +7,6 @@
 
 ## global settings
 
-LOGICS="HOL ZF"
 FAKE_BUILD=""
 DISTBASE=~/tmp/isadist
 ROOT=/usr/share
@@ -80,7 +79,8 @@
   touch heaps/${COMPILER}/HOL-Real
   touch heaps/${COMPILER}/ZF
 else
-  ./build -bi $LOGICS
+  ./build -b -m HOL-Real HOL
+  ./build -b ZF
   rm -f heaps/${COMPILER}/Pure heaps/${COMPILER}/FOL heaps/${COMPILER}/TLA
 fi
 
@@ -157,6 +157,12 @@
 syntactic and deductive tools available in generic Isabelle.  Isabelle
 proof tools provide a high degree of automation.
 
+By virtue of the Isabelle/Isar subsystem, interactive proof
+development may be performed both via traditional tactic scripts, or
+actual human readable (formal) proof texts.  The resulting theory
+developments may be presented in high quality as (PDF)LaTeX documents,
+accommodating both printed copies and WWW browsing.
+
 %package	HOL
 Summary:	Isabelle Theorem Proving Environment -- Higher-Order Logic
 Group:		Applications/Math