make-all-poly
author nipkow
Tue May 09 22:10:08 1995 +0200 (1995-05-09)
changeset 1114 c8dfb56a7e95
parent 699 2da262e85c4d
permissions -rwxr-xr-x
Prod is now a parent of Lfp.
Added thm induct2 to Lfp.
Changed the way patterns in abstractions are pretty printed.
It has become simpler now but fails if split has more than one argument
because then the ast-translation does not match.
lcp@370
     1
#! /bin/sh
lcp@699
     2
#$Id$
lcp@370
     3
#Make entire system using Poly/ML
lcp@370
     4
#Pathnames will have to be modified for your site
lcp@699
     5
ML_DBASE=/usr/groups/theory/poly/polyml/`arch`/ML_dbase
lcp@699
     6
ISABELLEBIN=/homes/`whoami`/dbases
lcp@370
     7
ISABELLECOMP="poly -noDisplay -h 15000"
lcp@547
     8
export ML_DBASE ISABELLEBIN ISABELLECOMP 
lcp@370
     9
nohup make-all $*