src/HOL/Tools/specification_package.ML
2006-10-09 ago attribute: Context.mapping;
2006-09-15 ago renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-08-05 ago avoid low-level tsig;
2006-06-13 ago tuned;
2006-05-07 ago removed 'concl is' patterns;
2006-04-13 ago Sign.typ_equiv;
2006-02-03 ago canonical member/insert/merge;
2006-01-27 ago moved theorem tags from Drule to PureThy;
2006-01-25 ago ObjectLogic.atomize_cterm;
2006-01-21 ago simplified type attribute;
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 ago oriented result pairs in PureThy
2005-12-06 ago re-oriented some result tuples in PureThy
2005-10-18 ago moved helper lemma to HilbertChoice.thy;
2005-09-14 ago introduced AList.lookup
2005-09-13 ago tuned IsarThy.theorem_i;
2005-08-16 ago OuterKeyword;
2005-05-09 ago choice_const moved to hologic.ML
2005-04-21 ago Adapted to new interface of instantiation and unification / matching functions.
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-05-21 ago Sign.typ_instance;
2004-04-17 ago Minor cleanup of headers and some speedup of the HOL4 import.
2003-10-09 ago Added support for making constants final, that is, ensuring that no
2003-10-08 ago Added axiomatic specifications (ax_specification).
2003-08-27 ago Improved the error messages (slightly).
2003-08-26 ago Cleaned up the code.
2003-08-26 ago Allowed for splitting the specification over several lemmas.
2003-07-21 ago Added handling of meta implication and meta quantification.
2003-07-21 ago Added handling of free variables (provided they are of sort HOL.type).
2003-07-21 ago Changed bstring argument to xstring.
2003-07-21 ago *** empty log message ***
2003-07-19 ago Added optional theorem names for the constant definitions added during
2003-07-17 ago Added package for definition by specification.