change_simp
author nipkow
Tue, 09 May 1995 22:10:08 +0200
changeset 1114 c8dfb56a7e95
parent 9 c1795fac88c3
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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
     1
#! /bin/sh
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
     2
#    simp FILE1 ... FILEn
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
     3
#
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
     4
#  leaves previous versions as XXX~~
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
     5
#
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
     6
for f in $*
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
     7
do
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
     8
echo $f. \ Backup file is $f~~
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
     9
mv $f $f~~; sed -e '
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
    10
s/\<ASM_SIMP_TAC\>/asm_simp_tac/g
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
    11
s/\<SIMP_TAC\>/simp_tac/g
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
    12
s/\<addrews\>/addsimps/g
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
    13
s/addsplits \(\[[^]]*\]\)/setloop (split_tac \1)/g
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
    14
s/addsplits/setloop  split_tac/g
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
    15
s/\<setauto\>/setsolver/g
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
    16
' $f~~ > $f
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
    17
done
c1795fac88c3 make-all now has set +e so that New Jersey runs will continue even if some
lcp
parents:
diff changeset
    18
echo Finished.