# HG changeset patch
# User lcp
# Date 748543185 -7200
# Node ID c1795fac88c3c15380682e70bb83743f1c1ce586
# Parent  c3d2c6dcf3f0852c053cdb2c4bea62fd60100838
make-all now has set +e so that New Jersey runs will continue even if some
logic fails.  change_simp added to help change to new simplifier.

diff -r c3d2c6dcf3f0 -r c1795fac88c3 change_simp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/change_simp	Mon Sep 20 18:39:45 1993 +0200
@@ -0,0 +1,18 @@
+#! /bin/sh
+#    simp FILE1 ... FILEn
+#
+#  leaves previous versions as XXX~~
+#
+for f in $*
+do
+echo $f. \ Backup file is $f~~
+mv $f $f~~; sed -e '
+s/\<ASM_SIMP_TAC\>/asm_simp_tac/g
+s/\<SIMP_TAC\>/simp_tac/g
+s/\<addrews\>/addsimps/g
+s/addsplits \(\[[^]]*\]\)/setloop (split_tac \1)/g
+s/addsplits/setloop  split_tac/g
+s/\<setauto\>/setsolver/g
+' $f~~ > $f
+done
+echo Finished.
diff -r c3d2c6dcf3f0 -r c1795fac88c3 make-all
--- a/make-all	Mon Sep 20 17:02:11 1993 +0200
+++ b/make-all	Mon Sep 20 18:39:45 1993 +0200
@@ -57,6 +57,8 @@
     on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL Cube FOLP)
 esac
 
+set +e			#no longer fail upon errors -- e.g. if a "make" fails
+
 echo
 echo
 echo '*****Pure Isabelle*****'
diff -r c3d2c6dcf3f0 -r c1795fac88c3 src/Tools/change_simp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/change_simp	Mon Sep 20 18:39:45 1993 +0200
@@ -0,0 +1,18 @@
+#! /bin/sh
+#    simp FILE1 ... FILEn
+#
+#  leaves previous versions as XXX~~
+#
+for f in $*
+do
+echo $f. \ Backup file is $f~~
+mv $f $f~~; sed -e '
+s/\<ASM_SIMP_TAC\>/asm_simp_tac/g
+s/\<SIMP_TAC\>/simp_tac/g
+s/\<addrews\>/addsimps/g
+s/addsplits \(\[[^]]*\]\)/setloop (split_tac \1)/g
+s/addsplits/setloop  split_tac/g
+s/\<setauto\>/setsolver/g
+' $f~~ > $f
+done
+echo Finished.
diff -r c3d2c6dcf3f0 -r c1795fac88c3 src/Tools/make-all
--- a/src/Tools/make-all	Mon Sep 20 17:02:11 1993 +0200
+++ b/src/Tools/make-all	Mon Sep 20 18:39:45 1993 +0200
@@ -57,6 +57,8 @@
     on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL Cube FOLP)
 esac
 
+set +e			#no longer fail upon errors -- e.g. if a "make" fails
+
 echo
 echo
 echo '*****Pure Isabelle*****'