src/HOL/HOL.thy
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-15 wenzelm 2010-05-15 incorporated further conversions and conversionals, after some minor tuning;
2010-05-09 wenzelm 2010-05-09 just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-04 berghofe 2010-05-04 merged
2010-05-04 berghofe 2010-05-04 induct_true_def and induct_false_def are already contained in induct_rulify_fallback.
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-04-29 wenzelm 2010-04-29 proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-04-29 haftmann 2010-04-29 avoid popular infixes
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-04-26 huffman 2010-04-26 merged
2010-04-26 huffman 2010-04-26 syntax precedence for If and Let
2010-04-25 wenzelm 2010-04-25 renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp; less pervasive names;
2010-04-23 wenzelm 2010-04-23 removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;
2010-04-21 bulwahn 2010-04-21 added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-29 blanchet 2010-03-29 reintroduce efficient set structure to collect "no_atp" theorems
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-17 blanchet 2010-03-17 fix typo in "nitpick_choice_spec" attribute name (singular, not plural)
2010-03-17 blanchet 2010-03-17 added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-01 haftmann 2010-03-01 merged
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-26 wenzelm 2010-02-26 tuned hyp_subst_tac';
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2010-01-31 berghofe 2010-01-31 merged
2010-01-30 berghofe 2010-01-30 Added setup for simplification of equality constraints in cases rules.
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2010-01-15 berghofe 2010-01-15 merged
2010-01-10 berghofe 2010-01-10 Added setup for simplification of equality constraints in induction rules.
2010-01-13 haftmann 2010-01-13 some syntax setup for Scala
2010-01-11 haftmann 2010-01-11 tuned code equations
2010-01-08 haftmann 2010-01-08 boolean operators for scala
2010-01-08 haftmann 2010-01-08 a primitive scala serializer
2009-12-30 krauss 2009-12-30 killed a few warnings
2009-12-07 haftmann 2009-12-07 split off evaluation mechanisms in separte module Code_Eval
2009-11-24 wenzelm 2009-11-24 some rearangement of load order to keep preferences adjacent -- slightly fragile;
2009-11-19 bulwahn 2009-11-19 replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
2009-11-10 wenzelm 2009-11-10 removed unused Quickcheck_RecFun_Simps;
2009-11-08 wenzelm 2009-11-08 modernized structure Reorient_Proc; explicit merge of constituent functions, avoids exponential blowup when traversing the import graph; adapted Theory_Data; tuned;
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-10-30 haftmann 2009-10-30 tuned code setup
2009-10-29 wenzelm 2009-10-29 modernized some structure names;
2009-10-29 wenzelm 2009-10-29 separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
2009-10-26 haftmann 2009-10-26 tuned code setup for primitive boolean connectors
2009-10-23 haftmann 2009-10-23 turned off old quickcheck
2009-10-21 blanchet 2009-10-21 renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
2009-10-20 paulson 2009-10-20 Removal of the unused atpset concept, the atp attribute and some related code.
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-28 wenzelm 2009-09-28 misc tuning and modernization;
2009-09-28 wenzelm 2009-09-28 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
2009-09-23 bulwahn 2009-09-23 added first prototype of the extended predicate compiler
2009-09-23 bulwahn 2009-09-23 experimenting to add some useful interface for definitions
2009-09-23 bulwahn 2009-09-23 added predicate compile preprocessing structure for definitional thms -- probably is replaced by hooking the theorem command differently
2009-09-09 haftmann 2009-09-09 moved eq handling in nbe into separate oracle
2009-08-26 boehmes 2009-08-26 added further conversions and conversionals
2009-07-24 wenzelm 2009-07-24 renamed functor BlastFun to Blast, require explicit theory; eliminated src/FOL/blastdata.ML;
2009-07-24 wenzelm 2009-07-24 renamed functor ProjectRuleFun to Project_Rule; renamed structure ProjectRule to Project_Rule;
2009-07-24 wenzelm 2009-07-24 renamed functor InductFun to Induct;