src/HOL/HOL.thy
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
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-08 haftmann 2006-11-08 moved lemma eq_neq_eq_imp_neq to HOL
2006-11-07 wenzelm 2006-11-07 tuned hypsubst setup;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-11-05 wenzelm 2006-11-05 Sign.const_syntax_name;
2006-11-03 haftmann 2006-11-03 simplified reasoning tools setup
2006-10-31 haftmann 2006-10-31 added Equals_conv
2006-10-16 haftmann 2006-10-16 moved HOL code generator setup to Code_Generator
2006-10-13 haftmann 2006-10-13 lifted claset setup from ML to Isar level
2006-10-11 haftmann 2006-10-11 cleaned up HOL bootstrap
2006-10-10 haftmann 2006-10-10 cleanup basic HOL bootstrap
2006-10-02 haftmann 2006-10-02 improved serialization for arbitrary
2006-09-28 wenzelm 2006-09-28 tuned;
2006-09-27 wenzelm 2006-09-27 proper const_syntax for uminus, abs;
2006-09-26 haftmann 2006-09-26 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-25 haftmann 2006-09-25 added 'undefined' serializer
2006-09-19 haftmann 2006-09-19 introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
2006-09-01 haftmann 2006-09-01 final syntax for some Isar code generator keywords
2006-08-14 haftmann 2006-08-14 simplified code generator setup
2006-07-27 wenzelm 2006-07-27 tuned proofs;
2006-07-21 berghofe 2006-07-21 - Added new "undefined" constant - normalization_conv no longer expects term to have form "Trueprop ..."
2006-07-07 nipkow 2006-07-07 made evaluation_conv and normalization_conv visible.
2006-07-05 paulson 2006-07-05 removed the "tagging" feature
2006-06-30 nipkow 2006-06-30 normalization uses refl now
2006-06-29 nipkow 2006-06-29 new method "normalization"
2006-06-14 haftmann 2006-06-14 slight adaption for code generator
2006-06-06 wenzelm 2006-06-06 quoted "if";
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-05-09 haftmann 2006-05-09 introduced characters for code generator; some improved code lemmas for some list functions
2006-05-09 haftmann 2006-05-09 different object logic setup for CodegenTheorems
2006-05-02 wenzelm 2006-05-02 replaced syntax/translations by abbreviation;
2006-04-06 haftmann 2006-04-06 adapted for definitional code generation
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2006-03-02 paulson 2006-03-02 moved the "use" directive
2006-03-01 mengj 2006-03-01 Added setup for "atpset" (a rule set for ATPs).
2006-02-25 haftmann 2006-02-25 improved codegen bootstrap
2006-02-22 wenzelm 2006-02-22 simplified Pure conjunction;
2006-02-14 haftmann 2006-02-14 added theory of executable rational numbers
2006-02-01 berghofe 2006-02-01 Added "evaluation" method and oracle.
2006-01-31 haftmann 2006-01-31 added serialization for arbitrary
2006-01-29 wenzelm 2006-01-29 declare 'defn' rules;
2006-01-23 haftmann 2006-01-23 removed problematic keyword 'atom'