wenzelm [Thu, 19 May 1994 16:25:03 +0200] rev 388
(replaces Thy/scan.ML)
scanner now based on combinators of structure Scanner;
improved handling of keywords;
now supports long.ids, (* (* nested *) comments *), {| verbatim text |};
wenzelm [Thu, 19 May 1994 16:22:48 +0200] rev 387
new datatype theory, supports 'draft theories' and incremental extension:
add_classes, add_defsort, add_types, add_tyabbrs, add_tyabbrs_i,
add_arities, add_consts, add_consts_i, add_syntax, add_syntax_i,
add_trfuns, add_trrules, add_axioms, add_axioms_i, add_thyname;
added merge_thy_list for multiple merges and extend-merges;
added rep_theory, subthy, eq_thy, cert_axm, read_axm;
changed type of axioms_of;
renamed internal merge_theories to merge_thm_sgs;
various internal changes of thm and theory related code;
wenzelm [Thu, 19 May 1994 16:20:52 +0200] rev 386
added const_type: sg -> typ option;
stamps now stored in REVERSE order;
now supports 'draft signatures' and incremental extension: is_draft,
add_classes (supports axclasses), add_defsort, add_types, add_tyabbrs,
add_tyabbrs_i, add_arities, add_consts, add_consts_i, add_syntax,
add_syntax_i, add_trfuns, add_trrules, add_name, make_draft;
added const_of_class, class_of_const (for axclasses);
changed the pure signature to support axclasses (added itself, TYPE);
various major internal changes;