src/Pure/sign.ML
2007-10-11 wenzelm 2007-10-11 replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-10 wenzelm 2007-10-10 generalized notation interface (add or del);
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations; existing pretty_term = Syntax.pretty_term o ProofContext.init etc.; removed pretty_classrel/arity (cf. Syntax/syntax.ML);
2007-09-30 wenzelm 2007-09-30 add_consts_authentic/add_abbrev: tags (Markup.property list); tuned signature;
2007-09-29 wenzelm 2007-09-29 removed obsolete external interface add_const_constraint; removed redundant const_constraint; renamed add_const_constraint_i to add_const_constraint;
2007-09-26 wenzelm 2007-09-26 added minimize_sort, complete_sort;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-09-22 wenzelm 2007-09-22 certify': proper do_expand argument (which observes force_expand consts) instead of home-grown normalize;
2007-09-01 wenzelm 2007-09-01 read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;
2007-08-30 wenzelm 2007-08-30 infer_types: general check_typs instead of Type.cert_typ_mode;
2007-08-20 wenzelm 2007-08-20 read_def_terms: moved disambig to syntax.ML;
2007-08-14 wenzelm 2007-08-14 replaced certify_typ_syntax/abbrev by certify_typ_mode; removed obsolete read_sort', read_typ', read_typ_syntax', read_typ_abbrev';
2007-08-14 wenzelm 2007-08-14 PrimitiveDefs.dest_def; Syntax.standard_read;
2007-08-12 wenzelm 2007-08-12 read_def_terms': restrict scope of disambiguation to individual term;
2007-08-03 wenzelm 2007-08-03 certify: no check_thy here;
2007-07-24 wenzelm 2007-07-24 moved exception capture/release to structure Exn;
2007-07-09 wenzelm 2007-07-09 type output = string indicates raw system output;
2007-07-07 wenzelm 2007-07-07 simplified pretty token metric: type int;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-26 wenzelm 2007-04-26 renamed some old names Theory.xxx to Sign.xxx;
2007-04-26 wenzelm 2007-04-26 renamed some old names Theory.xxx to Sign.xxx;
2007-04-21 wenzelm 2007-04-21 export get_sort (belongs to Syntax module);
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;