src/HOL/HOL.thy
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-30 hoelzl 2014-10-30 disable coercions for NO_MATCH
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-10-24 hoelzl 2014-10-24 move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
2014-10-13 wenzelm 2014-10-13 Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-08-16 wenzelm 2014-08-16 modernized module name and setup;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-05-12 wenzelm 2014-05-12 tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
2014-04-03 blanchet 2014-04-03 use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
2014-02-26 haftmann 2014-02-26 prefer proof context over background theory
2014-02-20 wenzelm 2014-02-20 modernized tool setup; tuned;
2014-02-10 wenzelm 2014-02-10 discontinued axiomatic 'classes', 'classrel', 'arities';
2014-02-10 wenzelm 2014-02-10 more explicit axiomatization;
2014-02-01 wenzelm 2014-02-01 more standard file/module names;
2014-01-01 haftmann 2014-01-01 fundamental treatment of undefined vs. universally partial replaces code_abort
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-08-22 haftmann 2013-08-22 congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj
2013-07-14 wenzelm 2013-07-14 recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;
2013-07-13 wenzelm 2013-07-13 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-23 wenzelm 2013-06-23 tuned message -- more markup;
2013-05-30 wenzelm 2013-05-30 standardized aliases;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 wenzelm 2013-04-10 tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side; declare command "print_case_translations" where it is actually defined;
2013-04-10 wenzelm 2013-04-10 merged
2013-04-10 wenzelm 2013-04-10 discontinued obsolete ML antiquotation @{claset};
2013-01-22 traytel 2013-01-22 separate data used for case translation from the datatype package
2013-02-28 wenzelm 2013-02-28 just one HOLogic.Trueprop_conv, with regular exception CTERM; tuned;
2013-02-28 wenzelm 2013-02-28 marginalized historic strip_tac;
2013-02-06 hoelzl 2013-02-06 check alpha equality after applying beta and eta conversion in let-simproc, otherwise the simplifier may loop
2012-12-05 nipkow 2012-12-05 \<noteq> now has the same associativity as ~= and =
2012-09-12 wenzelm 2012-09-12 eliminated some old material that is unused in the visible universe;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-08-11 wenzelm 2012-08-11 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
2012-07-05 wenzelm 2012-07-05 removed obsolete rev_contrapos (cf. 1d195de59497);
2012-06-05 haftmann 2012-06-05 prefer sys.error over plain error in Scala to avoid deprecation warning
2012-04-19 haftmann 2012-04-19 moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
2012-03-16 wenzelm 2012-03-16 modernized axiomatization; eliminated odd 'finalconsts';
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2012-01-11 wenzelm 2012-01-11 more conventional eval_tac vs. method_setup "eval"; clarified method "normalization": THEN_ALL_NEW avoids bumping into other subgoals;
2012-01-09 wenzelm 2012-01-09 prefer antiquotations;
2012-01-05 wenzelm 2012-01-05 improved case syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;
2011-11-27 wenzelm 2011-11-27 more antiquotations;
2011-11-24 wenzelm 2011-11-24 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-10-28 wenzelm 2011-10-28 tuned Named_Thms: proper binding;
2011-10-21 bulwahn 2011-10-21 replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
2011-10-19 bulwahn 2011-10-19 removing old code generator setup in the HOL theory
2011-10-12 wenzelm 2011-10-12 modernized structure Induct_Tacs;
2011-09-20 nipkow 2011-09-20 New proof method "induction" that gives induction hypotheses the name IH.
2011-09-13 huffman 2011-09-13 tuned proofs