src/ZF/Tools/typechk.ML
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-08-27 wenzelm 2014-08-27 more explicit Method.modifier with reported position;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-09 wenzelm 2013-04-09 discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;
2013-03-30 wenzelm 2013-03-30 more item markup; tuned signature;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2011-06-29 wenzelm 2011-06-29 tuned signature;
2011-06-29 wenzelm 2011-06-29 simplified/unified Simplifier.mk_solver;
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2011-04-20 wenzelm 2011-04-20 eliminated Display.string_of_thm_without_context; tuned whitespace;
2010-08-18 haftmann 2010-08-18 deglobalization
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-02-28 wenzelm 2010-02-28 more antiquotations; eliminated legacy ML bindings;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-07-24 wenzelm 2009-07-24 tuned;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-15 wenzelm 2009-03-15 simplified method setup;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset;
2008-03-15 wenzelm 2008-03-15 proper antiquotations;
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
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