src/Pure/sign.ML
2008-03-14 haftmann 2008-03-14 added mk_const functions
2007-11-27 wenzelm 2007-11-27 standard_parse_term: check ambiguous results without changing the result yet;
2007-11-23 haftmann 2007-11-23 separated typedecl module, providing typedecl command with interpretation
2007-11-11 wenzelm 2007-11-11 syntax operations: turned extend'' into update'' (absorb duplicates);
2007-11-10 wenzelm 2007-11-10 notation: based on Syntax.update_const_gram (avoids duplicates);
2007-11-09 wenzelm 2007-11-09 tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;
2007-11-08 wenzelm 2007-11-08 removed unused read_def_terms';
2007-11-07 wenzelm 2007-11-07 removed obsolete Sign.read_tyname/const (cf. ProofContext);
2007-10-20 wenzelm 2007-10-20 no_variables: tuned error msg;
2007-10-17 wenzelm 2007-10-17 removed unused set_policy;
2007-10-16 wenzelm 2007-10-16 add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again); added revert_abbrev;
2007-10-15 wenzelm 2007-10-15 renamed Consts.the_declaration to Consts.the_type;
2007-10-13 wenzelm 2007-10-13 add_abbrevs: unvarify result;
2007-10-11 wenzelm 2007-10-11 dest/cert_def: replaced Pretty.pp by explicit Proof.context;
2007-10-11 wenzelm 2007-10-11 tuned;
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;