agrep

renamed 'defns' to 'defs';
removed 'sigclass';
replaced parents by enclose;
exported parens, brackets, mk_list, mk_big_list, mk_pair, mk_triple;
various minor internal changes;

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