src/Pure/sign.ML
2006-11-09 wenzelm 2006-11-09 abbrevs: return result;
2006-11-07 wenzelm 2006-11-07 replaced const_syntax by notation, which operates on terms;
2006-11-05 wenzelm 2006-11-05 added const_syntax_name;
2006-09-29 wenzelm 2006-09-29 Syntax.mode;
2006-09-28 wenzelm 2006-09-28 consts: syntax consts only for actual syntax;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-08-03 wenzelm 2006-08-03 tuned;
2006-07-27 wenzelm 2006-07-27 read_def_cterms (legacy version): Consts.certify;
2006-07-26 wenzelm 2006-07-26 moved pprint functions to Isar/proof_display.ML;
2006-07-19 wenzelm 2006-07-19 Sign.infer_types: Name.context;
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
2006-05-17 wenzelm 2006-05-17 consts: replaced early'' flag by inverted authentic''; tuned interfaces;
2006-05-17 wenzelm 2006-05-17 always preserve authentic consts -- removed Syntax.mixfix_const;
2006-05-16 wenzelm 2006-05-16 added add_const_syntax, add_consts_authentic; tuned interface;
2006-05-16 wenzelm 2006-05-16 more abstract interface to classes/arities;
2006-04-30 wenzelm 2006-04-30 removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity); added primitive_class/classrel/arity;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-25 wenzelm 2006-04-25 added arity_number/sorts; tuned;
2006-04-13 wenzelm 2006-04-13 added typ_equiv; read_class: improved error;
2006-04-11 wenzelm 2006-04-11 added super_classes (from sorts.ML); removed read/cert_classrel (see axclass.ML);
2006-04-10 wenzelm 2006-04-10 Term.itselfT;
2006-04-09 wenzelm 2006-04-09 abbrevs: mode does not affect name space;
2006-04-08 wenzelm 2006-04-08 pretty_term': early vs. late externing (support authentic syntax); add_abbrevs(_i): support print mode and authentic syntax;
2006-03-18 wenzelm 2006-03-18 export arities_of instead of classes_arities_of;
2006-03-14 wenzelm 2006-03-14 declared_const: check for type constraint only, i.e. admit abbreviations as well; added del_trrules(_i);
2006-03-11 wenzelm 2006-03-11 got rid of type Sign.sg;
2006-03-11 wenzelm 2006-03-11 added read_class, read/cert_classrel/arity (from axclass.ML);
2006-02-17 wenzelm 2006-02-17 add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
2006-02-15 wenzelm 2006-02-15 replaced qualified_force_prefix to sticky_prefix;
2006-02-11 wenzelm 2006-02-11 removed custom_accesses; added qualified_force_prefix;
2006-02-10 wenzelm 2006-02-10 tuned extern_term, pretty_term';
2006-02-07 wenzelm 2006-02-07 export consts_of; removed const_expansion; pretty_term', infer_types(_simult): separate Consts.T argument; added generic certify; simplified certify_term/prop;
2006-02-06 wenzelm 2006-02-06 added add_abbrevs(_i); moved const_of_class/class_of_const to logic.ML; added no_vars (from theory.ML); added cert_def; added const_expansion; certify: refer to Consts.certify, which includes expansion;
2006-02-06 haftmann 2006-02-06 subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2006-02-02 wenzelm 2006-02-02 added specific map_typ/term (from term.ML);
2006-01-31 wenzelm 2006-01-31 advanced translations: Context.generic;
2006-01-19 wenzelm 2006-01-19 Syntax.basic_syn;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-13 wenzelm 2006-01-13 tuned;
2005-11-14 wenzelm 2005-11-14 added const_instance;
2005-11-10 wenzelm 2005-11-10 uncurried Consts.typargs;
2005-11-02 wenzelm 2005-11-02 moved consts declarations to consts.ML;
2005-10-28 wenzelm 2005-10-28 certify_term: tuned monomorphic consts;
2005-10-27 wenzelm 2005-10-27 consts: monomorphic;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-15 wenzelm 2005-09-15 extend: NameSpace.default_naming;
2005-09-13 wenzelm 2005-09-13 added hide_names(_i) (from isar_thy.ML);
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-31 wenzelm 2005-08-31 tuned classes_arities_of;
2005-08-29 wenzelm 2005-08-29 use AList operations;
2005-08-18 wenzelm 2005-08-18 added interfaces for compile translation functions (from Isar/isar_thy.ML);
2005-08-09 haftmann 2005-08-09 added selectors 'classes_of' and 'classes_arities_of'
2005-08-09 haftmann 2005-08-09 added 'the_const_constraint'
2005-08-01 wenzelm 2005-08-01 Compress.typ;
2005-07-28 wenzelm 2005-07-28 added add_const_constraint(_i), const_constraint; added typ_match, typ_unify;
2005-07-19 wenzelm 2005-07-19 Inttab.defined;
2005-07-06 wenzelm 2005-07-06 Context.check_thy;
2005-07-01 wenzelm 2005-07-01 added all_sorts_nonempty;