agrep

added incremental extension functions: extend_log_types, extend_type_gram,
extend_const_gram, extend_consts, extend_trfuns, extend_trrules;
replaced merge by merge_syntaxes;
various minor internal changes;

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