tuned;
authorwenzelm
Wed Sep 20 21:20:01 2000 +0200 (2000-09-20)
changeset 100391eb980d64ba3
parent 10038 839340b78fc8
child 10040 4642c9d62aeb
tuned;
Admin/makerpm
     1.1 --- a/Admin/makerpm	Wed Sep 20 14:59:19 2000 +0200
     1.2 +++ b/Admin/makerpm	Wed Sep 20 21:20:01 2000 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  ## global settings
     1.6  
     1.7 -LOGICS="HOL ZF"
     1.8  FAKE_BUILD=""
     1.9  DISTBASE=~/tmp/isadist
    1.10  ROOT=/usr/share
    1.11 @@ -80,7 +79,8 @@
    1.12    touch heaps/${COMPILER}/HOL-Real
    1.13    touch heaps/${COMPILER}/ZF
    1.14  else
    1.15 -  ./build -bi $LOGICS
    1.16 +  ./build -b -m HOL-Real HOL
    1.17 +  ./build -b ZF
    1.18    rm -f heaps/${COMPILER}/Pure heaps/${COMPILER}/FOL heaps/${COMPILER}/TLA
    1.19  fi
    1.20  
    1.21 @@ -157,6 +157,12 @@
    1.22  syntactic and deductive tools available in generic Isabelle.  Isabelle
    1.23  proof tools provide a high degree of automation.
    1.24  
    1.25 +By virtue of the Isabelle/Isar subsystem, interactive proof
    1.26 +development may be performed both via traditional tactic scripts, or
    1.27 +actual human readable (formal) proof texts.  The resulting theory
    1.28 +developments may be presented in high quality as (PDF)LaTeX documents,
    1.29 +accommodating both printed copies and WWW browsing.
    1.30 +
    1.31  %package	HOL
    1.32  Summary:	Isabelle Theorem Proving Environment -- Higher-Order Logic
    1.33  Group:		Applications/Math