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