src/Pure/sign.ML
1993-11-25 wenzelm 1993-11-25 Sign.extend: Syntax.extend now called with read_ty;
1993-10-04 wenzelm 1993-10-04 Pure/ROOT.ML cleaned comments; removed extraneous 'print_depth 1'; replaced Basic_Syntax by BasicSyntax added 'use "install_pp.ML"'; Pure/README fixed comments; Pure/POLY.ML Pure/NJ.ML make_pp: added fbrk; Pure/install_pp.ML replaced "Ast" by "Syntax"; Pure/sign.ML added 'quote' to some error msgs;
1993-09-16 clasohm 1993-09-16 Initial revision