src/HOL/HOL.thy
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;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-21 haftmann 2009-07-21 moved abstract algebra section to the end
2009-07-14 haftmann 2009-07-14 tuned code annotations
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-07-07 haftmann 2009-07-07 more accurate certificates for constant aliasses
2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-06-25 haftmann 2009-06-25 arbitrary farewell
2009-05-30 wenzelm 2009-05-30 modernized method setup;
2009-05-16 bulwahn 2009-05-16 merged
2009-05-16 bulwahn 2009-05-16 added collection of simplification rules of recursive functions for quickcheck
2009-05-16 nipkow 2009-05-16 "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".
2009-05-14 haftmann 2009-05-14 merged module code_unit.ML into code.ML
2009-05-14 haftmann 2009-05-14 rewrite op = == eq handled by simproc
2009-05-13 haftmann 2009-05-13 itself is instance of eq
2009-05-12 haftmann 2009-05-12 transferred code generator preprocessor into separate module
2009-04-29 huffman 2009-04-29 reimplement reorientation simproc using theory data
2009-04-25 wenzelm 2009-04-25 misc cleanup of auto_solve and quickcheck: tools are in src/Tools and loaded uniformly in HOL; preferences are configured in their proper place -- despite old misleading comments in the source; use predefined preferences categories; setmp preferences in-place;
2009-04-24 haftmann 2009-04-24 generic postprocessing scheme for term evaluations
2009-04-23 haftmann 2009-04-23 avoid local [code]
2009-04-17 haftmann 2009-04-17 re-engineering of evaluation conversions
2009-04-15 haftmann 2009-04-15 code generator bootstrap theory src/Tools/Code_Generator.thy
2009-04-15 haftmann 2009-04-15 wrecked old code_funcgr module
2009-03-20 wenzelm 2009-03-20 Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-07 blanchet 2009-03-07 Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
2009-03-06 blanchet 2009-03-06 Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.