src/Pure/sign.ML
2007-04-15 wenzelm 2007-04-15 removed obsolete TypeInfer.logicT -- use dummyT;
2007-04-15 wenzelm 2007-04-15 removed obsolete infer_types(_simult); read_sort/get_sort, read_def_terms: internal reorganization;
2007-04-14 wenzelm 2007-04-14 read_typ_XXX: no sorts; added read_def_typ (formerly read_typ);
2007-01-19 wenzelm 2007-01-19 moved ML translation interfaces to isar_cmd.ML;
2007-01-19 wenzelm 2007-01-19 adapted ML context operations;
2006-12-29 wenzelm 2006-12-29 replaced classes by all_classes (topologically sorted); added minimal_classes;
2006-12-12 wenzelm 2006-12-12 add_abbrev: tuned signature;
2006-12-11 wenzelm 2006-12-11 advanced translation functions: Proof.context;
2006-12-10 wenzelm 2006-12-10 added no_frees; add_abbrev: tuned handling of frees, temp workaround;
2006-12-09 wenzelm 2006-12-09 tuned Consts signature;
2006-12-07 wenzelm 2006-12-07 simplified add_abbrev -- single argument;
2006-12-07 wenzelm 2006-12-07 simplified add_abbrevs: no mixfix;
2006-12-06 wenzelm 2006-12-06 add_abbrevs: moved common parts to consts.ML;
2006-12-05 wenzelm 2006-12-05 add_notation: permissive about undeclared consts;
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