2015-04-06 wenzelm 2015-04-06 local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-27 wenzelm 2015-03-27 tuned signature;
2015-03-24 wenzelm 2015-03-24 clarified case_tac fixes and context;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-09-17 blanchet 2014-09-17 support (finite values of) codatatypes in Quickcheck
2014-09-11 blanchet 2014-09-11 speed up old Nominal by killing type variables
2014-09-08 blanchet 2014-09-08 ported old Nominal to use new datatypes
2014-09-08 blanchet 2014-09-08 use compatibility layer
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-09-01 blanchet 2014-09-01 tuned structure inclusion
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2013-04-10 wenzelm 2013-04-10 formal proof context for axclass proofs; avoid global_simpset_of -- refer to simpset of proof context;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-01-10 berghofe 2012-01-10 Corrected pt_set_inst, added missing cp_set_inst, deleted obsolete pt_insert_eqvt, pt_set_eqvt, and perm_set_eq
2011-12-24 haftmann 2011-12-24 treatment of type constructor `set`
2011-12-13 wenzelm 2011-12-13 'datatype' specifications allow explicit sort constraints; tuned signatures;
2011-11-30 wenzelm 2011-11-30 discontinued obsolete datatype "alt_names";
2011-10-12 wenzelm 2011-10-12 modernized structure Induct_Tacs;
2011-09-03 haftmann 2011-09-03 tuned specifications
2011-09-03 haftmann 2011-09-03 assert Pure equations for theorem references; tuned
2011-01-15 berghofe 2011-01-15 Finally removed old primrec package, since Primrec.add_primrec_global can be used instead.
2010-12-15 wenzelm 2010-12-15 eliminated dead code;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-23 haftmann 2009-06-23 add_datatypes does not yield particular rules any longer
2009-06-23 haftmann 2009-06-23 add_datatype interface yields type names and less rules
2009-06-21 haftmann 2009-06-21 simplified names of common datatype types
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-17 haftmann 2009-06-17 datatype packages: record datatype_config for configuration flags; less verbose signatures
2009-05-07 haftmann 2009-05-07 explicit type_name antiquotations
2009-03-19 wenzelm 2009-03-19 proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in packages;
2009-03-04 nipkow 2009-03-04 Made Option a separate theory and renamed option_map to
2009-02-25 berghofe 2009-02-25 Added equivariance lemmas for fresh_star.
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2008-12-16 Christian Urban 2008-12-16 changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-10 berghofe 2008-11-10 Some more functions for accessing information about atoms.
2008-09-26 berghofe 2008-09-26 Added some more theorems to NominalData.
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-27 urbanc 2008-08-27 added equivariance lemmas for ex1 and the
2008-07-29 haftmann 2008-07-29 PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-06-30 urbanc 2008-06-30 added facts to lemma swap_simps and tuned lemma calc_atms
2008-06-14 wenzelm 2008-06-14 InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;
2008-06-10 wenzelm 2008-06-10 InductTacs.case_tac with proper context and proper declaration of local variable;
2008-06-10 haftmann 2008-06-10 polished interface of datatype package
2008-06-09 wenzelm 2008-06-09 adapted case_tac/induct_tac;
2008-05-07 berghofe 2008-05-07 - Deleted arity proofs for set - Produce specific instances of theorems insert_eqvt, set_eqvt and perm_set_eq
2008-05-02 urbanc 2008-05-02 added more infrastructure for fresh_star
2008-03-29 wenzelm 2008-03-29 eliminated non-linear access to thy1 and thy12c;