agrep
author lcp
Thu, 03 Nov 1994 16:39:41 +0100
changeset 695 a1586fa1b755
parent 0 a5a9c433f639
child 717 a52ba17ee9c5
permissions -rwxr-xr-x
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)

#! /bin/csh
grep "$*" {Pure/Syntax,Pure/Thy}/*ML */*ML */ex/*ML