src/Pure/sign.ML
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;
2005-06-29 wenzelm 2005-06-29 eliminated separate syn type -- advanced trfuns already part of Syntax.syntax;
2005-06-22 wenzelm 2005-06-22 renamed init to init_data;
2005-06-20 wenzelm 2005-06-20 added certify_prop, cert_term, cert_prop;
2005-06-17 wenzelm 2005-06-17 obsolete type sg is now an alias for Context.theory; code and interfaces related to stamps and data now in context.ML; actual signature content declared as theory data; removed type sg_ref (superceded by theory_ref); signature SIGN_THEORY lists theory operations that are duplicated in Theory;
2005-06-11 wenzelm 2005-06-11 discontinued named name spaces (classK, typeK, constK); name space of classes and types maintained in tsig; read_tyname/read_const now raise ERROR instead of TYPE; tuned;
2005-06-09 wenzelm 2005-06-09 simplified is_stale, check_stale; fixed map_sg -- proper treatment of non-drafts;
2005-06-09 wenzelm 2005-06-09 Major cleanup: got rid of types bclass, xclass, xsort, xtyp, xterm; reorganized code to separate stamps/data/sign; clarified name space inter/extern operations; sane read/certify operations -- more picky about stale signatures; sane implementation of signature extensions;
2005-06-05 wenzelm 2005-06-05 added the_const_type;
2005-06-02 wenzelm 2005-06-02 replaced set_naming by restore_naming;
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern; name entry path superceded by general naming context; added qualified_names, no_base_names, custom_accesses, set_policy, set_naming; replaced NameSpace.extend by context-dependent declare_name; removed full_name'; tuned;
2005-04-29 paulson 2005-04-29 better error reporting
2005-04-23 wenzelm 2005-04-23 improved read_tyname; merge_stamps, merge_refs: error instead of raise TERM;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-04-21 berghofe 2005-04-21 - Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.
2005-04-16 wenzelm 2005-04-16 added del_modesyntax(_i); added print_all_data;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** added declared_tyname/const and read_tyname/const; removed certify_tyname/const; added prep_ext_merge, nontriv_merge kept internal; efficient subsig test;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-24 ballarin 2005-03-24 Further work on interpretation commands. New command `interpret' for interpretation in proof contexts.