{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
solve the goal fully
#! /bin/sh#Make entire system using Poly/ML#Pathnames will have to be modified for your siteML_DBASE=/usr/groups/theory/poly/`arch`/ML_dbaseISABELLEBIN=/homes/`whoami`/binISABELLECOMP="poly -noDisplay -h 15000"export ML_DBASE ISABELLEBIN ISABELLECOMP nohup make-all $*