agrep
author lcp
Fri, 17 Sep 1993 16:16:38 +0200
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 717 a52ba17ee9c5
permissions -rwxr-xr-x
Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
#! /bin/csh
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
grep "$*" {Pure/Syntax,Pure/Thy}/*ML */*ML */ex/*ML