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'.
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;