src/HOL/HOL.thy
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.
2009-03-04 blanchet 2009-03-04 Second try at adding "nitpick_const_def" attribute. I don't know what happened the first time (change d8944fd4365e). It just vanished somehow.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-01 blanchet 2009-03-01 Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
2009-03-02 haftmann 2009-03-02 reduced confusion code_funcgr vs. code_wellsorted
2009-02-28 wenzelm 2009-02-28 moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
2009-02-28 wenzelm 2009-02-28 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
2009-02-22 haftmann 2009-02-22 experimental switch to new well-sorting algorithm
2009-02-22 haftmann 2009-02-22 formal dependency on newly emerging algorithm
2009-02-20 haftmann 2009-02-20 reverted to old wellsorting algorithm
2009-02-20 haftmann 2009-02-20 experimental inclusion of new wellsorting algorithm for code equations
2009-02-18 haftmann 2009-02-18 do not drop arguments to 0, 1
2009-02-10 blanchet 2009-02-10 Renamed descriptions of Nitpick (and ATP) attributes, so that they fit well with the rest of the sentence in ProofGeneral.
2009-02-09 blanchet 2009-02-09 Reintroduced nitpick_ind_intro attribute. It looks like I need it nonetheless.
2009-02-09 blanchet 2009-02-09 Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute. This should now be all.
2009-02-06 blanchet 2009-02-06 Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems; these will be used by Nitpick, which will be released independently of Isabelle 2009, but they need to be in.
2009-01-21 haftmann 2009-01-21 no base sort in class import
2009-01-16 haftmann 2009-01-16 added HOL-Base image
2008-12-15 haftmann 2008-12-15 moved value.ML to src/Tools
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-11-20 wenzelm 2008-11-20 Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-11-13 haftmann 2008-11-13 simproc for let
2008-10-28 ballarin 2008-10-28 Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.