agrep
author nipkow
Tue, 09 May 1995 22:10:08 +0200
changeset 1114 c8dfb56a7e95
parent 717 a52ba17ee9c5
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.

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