src/HOL/HOL.thy
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
2007-03-20 haftmann 2007-03-20 explizit "type" superclass
2007-03-18 dixon 2007-03-18 TrueElim and notTrueElim tested and added as safe elim rules.
2007-03-16 dixon 2007-03-16 removed safe elim flag of trueElim and notFalseElim for testing.
2007-03-16 dixon 2007-03-16 added safe intro rules for removing "True" subgoals as well as "~ False" ones.
2007-02-28 wenzelm 2007-02-28 tuned ML setup;
2007-01-31 haftmann 2007-01-31 dropped lemma duplicates in HOL.thy
2007-01-20 wenzelm 2007-01-20 tuned ML setup; added @{claset};
2006-12-06 wenzelm 2006-12-06 removed legacy ML bindings; simplified ML setup; tuned declarations;
2006-11-27 haftmann 2006-11-27 moved order arities for fun and bool to Fun/Orderings
2006-11-26 wenzelm 2006-11-26 updated (binder) syntax/notation;
2006-11-23 wenzelm 2006-11-23 tuned proofs;
2006-11-23 wenzelm 2006-11-23 prefer antiquotations over LaTeX macros;
2006-11-23 webertj 2006-11-23 typo in comment fixed
2006-11-18 haftmann 2006-11-18 tuned