src/HOL/HOL.thy
2007-10-04 ago moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-09-29 ago proper syntax during class specification
2007-09-18 ago moved Tools/integer.ML to Pure/General/integer.ML;
2007-09-07 ago added lemma
2007-09-01 ago final(?) iteration of sgn saga.
2007-08-28 ago codegen.ML is now loaded in Pure again.
2007-08-16 ago fixed codegen setup
2007-08-15 ago ATP blacklisting is now in theory data, attribute noatp
2007-08-15 ago updated code generator setup
2007-08-10 ago new structure for code generator modules
2007-08-07 ago new nbe implementation
2007-07-29 ago simplified ResAtpset via NamedThmsFun;
2007-07-24 ago using class target
2007-07-20 ago simplified HOL bootstrap
2007-07-04 ago replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
2007-07-03 ago use hologic.ML in basic HOL context;
2007-07-03 ago CONVERSION tactical;
2007-06-28 ago simplified keyword setup
2007-06-17 ago added Theorem all_not_ex
2007-06-14 ago tuned proofs: avoid implicit prems;
2007-06-05 ago tuned boostrap
2007-06-05 ago merged Code_Generator.thy into HOL.thy
2007-05-31 ago moved IsaPlanner from Provers to Tools;
2007-05-31 ago proper loading of ML files;
2007-05-19 ago added a set of NNF normalization lemmas and nnf_conv
2007-05-17 ago tuned
2007-05-06 ago dropped HOL.ML
2007-04-20 ago Isar definitions are now added explicitly to code theorem table
2007-03-20 ago added class "default" and expansion axioms for undefined
2007-03-20 ago explizit "type" superclass
2007-03-18 ago TrueElim and notTrueElim tested and added as safe elim rules.
2007-03-16 ago removed safe elim flag of trueElim and notFalseElim for testing.
2007-03-16 ago added safe intro rules for removing "True" subgoals as well as "~ False" ones.
2007-02-28 ago tuned ML setup;
2007-01-31 ago dropped lemma duplicates in HOL.thy
2007-01-20 ago tuned ML setup;
2006-12-06 ago removed legacy ML bindings;
2006-11-27 ago moved order arities for fun and bool to Fun/Orderings
2006-11-26 ago updated (binder) syntax/notation;
2006-11-23 ago tuned proofs;
2006-11-23 ago prefer antiquotations over LaTeX macros;
2006-11-23 ago typo in comment fixed
2006-11-18 ago tuned
2006-11-17 ago more robust syntax for definition/abbreviation/notation;
2006-11-08 ago moved lemma eq_neq_eq_imp_neq to HOL
2006-11-07 ago tuned hypsubst setup;
2006-11-07 ago renamed 'const_syntax' to 'notation';
2006-11-05 ago Sign.const_syntax_name;
2006-11-03 ago simplified reasoning tools setup
2006-10-31 ago added Equals_conv
2006-10-16 ago moved HOL code generator setup to Code_Generator
2006-10-13 ago lifted claset setup from ML to Isar level
2006-10-11 ago cleaned up HOL bootstrap
2006-10-10 ago cleanup basic HOL bootstrap
2006-10-02 ago improved serialization for arbitrary
2006-09-28 ago tuned;
2006-09-27 ago proper const_syntax for uminus, abs;
2006-09-26 ago renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-25 ago added 'undefined' serializer
2006-09-19 ago introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy