src/HOL/HOL.thy
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
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