2011-11-09 ago misc tuning;
2011-11-05 ago added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
2011-10-19 ago removed some remaining artefacts of ancient SML code generator
2011-07-06 ago prefer Synchronized.var;
2011-07-02 ago correction: do not assume that case const index covered all cases
2011-07-01 ago remove illegal case combinators after merge
2011-07-01 ago corrected misunderstanding what `old functions` are supposed to be
2011-07-01 ago centralized deletion of equations for constructors; corrected misunderstanding what `old functions` are supposed to be
2011-07-01 ago index cases for constructors
2011-06-09 ago tuned signature: Name.invent and Name.invent_names;
2011-06-09 ago simplified Name.variant -- discontinued builtin fold_map;
2011-05-06 ago improving merge of code specifications by removing code equations of constructors after merging two theories
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago prefer local name spaces;
2011-01-10 ago added merge_options convenience;
2011-01-08 ago misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-01 ago more direct use of binder_types/body_type;
2010-11-29 ago tuned
2010-11-27 ago typscheme with signatures is inappropriate when building empty certificate;
2010-11-27 ago corrected: use canonical variables of type scheme uniformly
2010-11-26 ago consider sort constraints for datatype constructors when constructing the empty equation certificate;
2010-11-26 ago keep type variable arguments of datatype constructors in bookkeeping
2010-11-16 ago added forall2 predicate lifter
2010-11-04 ago Code.check_const etc.: reject too specific types
2010-11-03 ago replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-10-26 ago more general treatment of type argument in code certificates for operations on abstract types
2010-10-01 ago chop_while replace drop_while and take_while
2010-09-30 ago take_while, drop_while
2010-09-30 ago corrected subsumption check: arguments have been reversed; addition of default equations to non-default equations is identity
2010-09-29 ago redundancy check: drop trailing Var arguments (avoids eta problems with equations)
2010-09-20 ago corrected long-overlooked slip: the Pure equality of a code equation is no part of the code equation itself
2010-09-20 ago more accurate exception handling
2010-09-15 ago ignore code cache optionally
2010-09-05 ago turned show_sorts/show_types into proper configuration options;
2010-09-01 ago replaced' by
2010-08-23 ago dropped now obsolete purge_data -- happens implicitly on change of theory identity
2010-06-24 ago made smlnj happy
2010-06-18 ago drop subsumed default equations (requires a little bit unfortunate laziness)
2010-06-17 ago explicit type variable arguments for constructors
2010-06-15 ago maintain cong rules for case combinators
2010-06-14 ago explicitly name and note equations for class eq
2010-05-03 ago renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-19 ago more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
2010-04-19 ago explicit check sorts in abstract certificates; abstractor is part of dependencies
2010-04-13 ago more accurate pattern match
2010-04-11 ago user interface for abstract datatypes is an attribute, not a command
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-07 ago modernized structure Local_Defs;
2010-02-26 ago use abstract code cerficates for bare code theorems
2010-02-24 ago bound argument for abstype proposition
2010-02-24 ago more precise exception handler
2010-02-22 ago more accurate when registering new types
2010-02-22 ago proper distinction of code datatypes and abstypes
2010-02-19 ago a simple concept for datatype invariants
2010-01-14 ago printing of cases
2010-01-13 ago explicit abstract type of code certificates
2010-01-13 ago corrected error messages; tuned
2010-01-12 ago code certificates as integral part of code generation