src/HOL/HOL.thy
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
2007-10-08 haftmann 2007-10-08 added first version of user-space type system for class target
2007-10-04 haftmann 2007-10-04 certificates for code generator case expressions
2007-10-04 haftmann 2007-10-04 clarified declarations in class ord
2007-10-04 wenzelm 2007-10-04 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-09-29 haftmann 2007-09-29 proper syntax during class specification
2007-09-18 wenzelm 2007-09-18 moved Tools/integer.ML to Pure/General/integer.ML;
2007-09-07 nipkow 2007-09-07 added lemma
2007-09-01 nipkow 2007-09-01 final(?) iteration of sgn saga.
2007-08-28 berghofe 2007-08-28 codegen.ML is now loaded in Pure again.
2007-08-16 haftmann 2007-08-16 fixed codegen setup
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-15 haftmann 2007-08-15 updated code generator setup
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-08-07 haftmann 2007-08-07 new nbe implementation
2007-07-29 wenzelm 2007-07-29 simplified ResAtpset via NamedThmsFun; proper simproc_setup for "neq", "let_simp";
2007-07-24 haftmann 2007-07-24 using class target
2007-07-20 haftmann 2007-07-20 simplified HOL bootstrap
2007-07-04 wenzelm 2007-07-04 replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
2007-07-03 wenzelm 2007-07-03 use hologic.ML in basic HOL context; tuned proofs;
2007-07-03 wenzelm 2007-07-03 CONVERSION tactical;
2007-06-28 haftmann 2007-06-28 simplified keyword setup
2007-06-17 chaieb 2007-06-17 added Theorem all_not_ex
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-06-05 haftmann 2007-06-05 tuned boostrap
2007-06-05 haftmann 2007-06-05 merged Code_Generator.thy into HOL.thy
2007-05-31 wenzelm 2007-05-31 moved IsaPlanner from Provers to Tools;
2007-05-31 wenzelm 2007-05-31 proper loading of ML files;
2007-05-19 chaieb 2007-05-19 added a set of NNF normalization lemmas and nnf_conv
2007-05-17 haftmann 2007-05-17 tuned
2007-05-06 haftmann 2007-05-06 dropped HOL.ML
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-03-20 haftmann 2007-03-20 added class "default" and expansion axioms for undefined