src/HOL/HOL.thy
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'.
2008-10-24 haftmann 2008-10-24 "arbitrary" merely abbreviates undefined
2008-10-22 haftmann 2008-10-22 code identifier namings are no longer imperative
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-07 haftmann 2008-10-07 re-introduces axiom subst
2008-09-29 haftmann 2008-09-29 polished code generator setup
2008-09-25 haftmann 2008-09-25 discontinued special treatment of op = vs. eq_class.eq
2008-09-22 berghofe 2008-09-22 Added setup for coherent logic prover.
2008-09-16 haftmann 2008-09-16 generic value command
2008-08-28 haftmann 2008-08-28 restructured and split code serializer module
2008-08-27 haftmann 2008-08-27 tuned code generator setup
2008-07-14 krauss 2008-07-14 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
2008-06-24 wenzelm 2008-06-24 ML_Antiquote.value;
2008-06-23 wenzelm 2008-06-23 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
2008-06-14 wenzelm 2008-06-14 removed obsolete case_split_tac -- cannot work without;
2008-06-10 wenzelm 2008-06-10 eliminated obsolete case_split_thm -- use case_split; added case_split_tac (works without context); setup for induct_tacs.ML;
2008-06-10 haftmann 2008-06-10 localized Least in Orderings.thy
2008-05-18 wenzelm 2008-05-18 eliminated theory CPure;
2008-04-24 haftmann 2008-04-24 moved 'trivial classes' to foundation of code generator
2008-04-22 haftmann 2008-04-22 different handling of eq class for nbe
2008-04-22 haftmann 2008-04-22 constant HOL.eq now qualified
2008-04-15 wenzelm 2008-04-15 Sign.hide_const;
2008-04-08 krauss 2008-04-08 Generic conversion and tactic "atomize_elim" to convert elimination rules to the object logic
2008-04-04 haftmann 2008-04-04 postprocessing of equality
2008-04-02 haftmann 2008-04-02 explicit class "eq" for operational equality
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset;
2008-03-26 wenzelm 2008-03-26 pass imp_elim, swap to classical prover;
2008-01-25 haftmann 2008-01-25 dropped superfluous code theorems
2008-01-02 haftmann 2008-01-02 splitted class uminus from class minus
2007-12-22 wenzelm 2007-12-22 use random_word.ML earlier;
2007-12-05 haftmann 2007-12-05 simplified infrastructure for code generator operational equality
2007-11-28 wenzelm 2007-11-28 replaced typedecl interpretation by ObjectLogic.typedecl (based on base_sort);
2007-11-23 haftmann 2007-11-23 interpretation of typedecls: instantiation to class type
2007-11-11 wenzelm 2007-11-11 tuned specifications of 'notation';
2007-11-05 kleing 2007-11-05 move itself into HOL types
2007-10-16 haftmann 2007-10-16 global class syntax