tuned comment;
moved local syntax to local_syntax.ML;
common naming (for abbrevs and thms);
transfer: merge consts;
tuned pretty_term';
added polymorphic -- special case of generalize;
added add_abbrevs(_i);
read/cert: expand_consts;
Bool = FOL +
types bool 0
arities bool :: term
consts tt,ff :: "bool"
end