2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-01-10 wenzelm 2011-01-10 added merge_options convenience;
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-11-29 haftmann 2010-11-29 tuned
2010-11-27 haftmann 2010-11-27 typscheme with signatures is inappropriate when building empty certificate; prefer logical_typscheme over const_typargs; tuned
2010-11-27 haftmann 2010-11-27 corrected: use canonical variables of type scheme uniformly
2010-11-26 haftmann 2010-11-26 consider sort constraints for datatype constructors when constructing the empty equation certificate; actually consider sort constraints in constructor sets; dropped redundant bindings
2010-11-26 haftmann 2010-11-26 keep type variable arguments of datatype constructors in bookkeeping
2010-11-16 haftmann 2010-11-16 added forall2 predicate lifter
2010-11-04 haftmann 2010-11-04 Code.check_const etc.: reject too specific types
2010-11-03 wenzelm 2010-11-03 replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-10-26 haftmann 2010-10-26 more general treatment of type argument in code certificates for operations on abstract types
2010-10-01 haftmann 2010-10-01 chop_while replace drop_while and take_while
2010-09-30 haftmann 2010-09-30 take_while, drop_while
2010-09-30 haftmann 2010-09-30 corrected subsumption check: arguments have been reversed; addition of default equations to non-default equations is identity
2010-09-29 haftmann 2010-09-29 redundancy check: drop trailing Var arguments (avoids eta problems with equations)
2010-09-20 haftmann 2010-09-20 corrected long-overlooked slip: the Pure equality of a code equation is no part of the code equation itself
2010-09-20 haftmann 2010-09-20 more accurate exception handling
2010-09-15 haftmann 2010-09-15 ignore code cache optionally
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-09-01 haftmann 2010-09-01 replaced' by
2010-08-23 haftmann 2010-08-23 dropped now obsolete purge_data -- happens implicitly on change of theory identity
2010-06-24 haftmann 2010-06-24 made smlnj happy
2010-06-18 haftmann 2010-06-18 drop subsumed default equations (requires a little bit unfortunate laziness)
2010-06-17 haftmann 2010-06-17 explicit type variable arguments for constructors
2010-06-15 haftmann 2010-06-15 maintain cong rules for case combinators
2010-06-14 haftmann 2010-06-14 explicitly name and note equations for class eq
2010-05-03 wenzelm 2010-05-03 renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-19 haftmann 2010-04-19 more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
2010-04-19 haftmann 2010-04-19 explicit check sorts in abstract certificates; abstractor is part of dependencies
2010-04-13 haftmann 2010-04-13 more accurate pattern match
2010-04-11 haftmann 2010-04-11 user interface for abstract datatypes is an attribute, not a command
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-02-26 haftmann 2010-02-26 use abstract code cerficates for bare code theorems
2010-02-24 haftmann 2010-02-24 bound argument for abstype proposition
2010-02-24 haftmann 2010-02-24 more precise exception handler
2010-02-22 haftmann 2010-02-22 more accurate when registering new types
2010-02-22 haftmann 2010-02-22 proper distinction of code datatypes and abstypes
2010-02-19 haftmann 2010-02-19 a simple concept for datatype invariants
2010-01-14 haftmann 2010-01-14 printing of cases
2010-01-13 haftmann 2010-01-13 explicit abstract type of code certificates
2010-01-13 haftmann 2010-01-13 corrected error messages; tuned
2010-01-12 haftmann 2010-01-12 code certificates as integral part of code generation
2010-01-11 haftmann 2010-01-11 added code certificates
2010-01-05 haftmann 2010-01-05 avoid exporting Type.build_tsig
2010-01-04 haftmann 2010-01-04 code cache only persists on equal theories
2010-01-04 haftmann 2010-01-04 code cache without copy; tuned
2009-12-24 haftmann 2009-12-24 made sml/nj happy
2009-12-23 haftmann 2009-12-23 reduced code generator cache to the baremost minimum
2009-12-04 wenzelm 2009-12-04 merged, resolving minor conflict, and recovering sane state;
2009-12-04 wenzelm 2009-12-04 merged, resolving minor conflicts;
2009-12-04 haftmann 2009-12-04 merged
2009-11-30 haftmann 2009-11-30 dropped some unused bindings
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-12-02 haftmann 2009-12-02 crude support for type aliasses and corresponding constant signatures
2009-11-19 bulwahn 2009-11-19 replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules