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
2010-01-11 ago added code certificates
2010-01-05 ago avoid exporting Type.build_tsig
2010-01-04 ago code cache only persists on equal theories
2010-01-04 ago code cache without copy; tuned
2009-12-24 ago made sml/nj happy
2009-12-23 ago reduced code generator cache to the baremost minimum
2009-12-04 ago merged, resolving minor conflict, and recovering sane state;
2009-12-04 ago merged, resolving minor conflicts;
2009-12-04 ago merged
2009-11-30 ago dropped some unused bindings
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop