src/ZF/Tools/typechk.ML
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-03 wenzelm 2007-10-03 avoid unnamed infixes;
2007-07-29 wenzelm 2007-07-29 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic;
2006-07-25 wenzelm 2006-07-25 Drule.merge_rules;
2006-01-21 wenzelm 2006-01-21 simplified type attribute; removed obsolete tcset operations -- clean data/attribute/method setup;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-10-17 wenzelm 2005-10-17 added type_solver (uses Simplifier.the_context); removed obsolete context_type_solver;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-07-13 wenzelm 2005-07-13 improved Net interface;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2004-07-30 wenzelm 2004-07-30 added context type solver;
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-15 wenzelm 2001-11-15 added TCSET(') tacticals;
2001-11-14 wenzelm 2001-11-14 Isar attribute and method setup;
2001-11-08 wenzelm 2001-11-08 theory data: finish method;
1999-04-30 wenzelm 1999-04-30 theory data: copy;
1999-01-27 paulson 1999-01-27 new typechecking solver for the simplifier
1999-01-13 paulson 1999-01-13 datatype package improvements
1998-12-28 paulson 1998-12-28 moved from ZF to new subdirectory Tools