lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
#! /bin/sh#Make entire system using Standard ML of New Jersey#Pathnames will have to be modified for your siteISABELLEBIN=/homes/`whoami`/binISABELLECOMP=smlexport ISABELLEBIN ISABELLECOMP nohup make-all $*