src/HOL/HOL.thy
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
2011-08-18 haftmann 2011-08-18 moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-08-03 bulwahn 2011-08-03 removing the SML evaluator
2011-07-02 haftmann 2011-07-02 install case certificate for If after code_datatype declaration for bool
2011-06-29 wenzelm 2011-06-29 tuned signature;
2011-06-27 wenzelm 2011-06-27 ML antiquotations are managed as theory data, with proper name space and entity markup; clarified Name_Space.check;
2011-05-14 wenzelm 2011-05-14 simplified BLAST_DATA;
2011-05-14 wenzelm 2011-05-14 modernized functor names; tuned;
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2011-04-26 wenzelm 2011-04-26 simplified Blast setup;
2011-04-22 wenzelm 2011-04-22 misc tuning and simplification;
2011-04-22 wenzelm 2011-04-22 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61); tuned signature;
2011-04-22 wenzelm 2011-04-22 modernized Quantifier1 simproc setup;
2011-04-22 wenzelm 2011-04-22 clarified simpset setup; discontinued unused old-style FOL_css;
2011-04-20 wenzelm 2011-04-20 explicit context for Codegen.eval_term etc.;
2011-04-20 wenzelm 2011-04-20 merged
2011-04-20 bulwahn 2011-04-20 making the evaluation of HOL.implies lazy even in strict languages by mapping it to an if statement
2011-04-19 wenzelm 2011-04-19 eliminated Codegen.mode in favour of explicit argument;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-03-31 haftmann 2011-03-31 corrected infix precedence for boolean operators in Haskell
2011-03-22 wenzelm 2011-03-22 more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
2011-02-28 paulson 2011-02-28 declare ext [intro]: Extensionality now available by default
2011-02-23 noschinl 2011-02-23 setup case_product attribute in HOL and FOL
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2011-01-27 wenzelm 2011-01-27 CRITICAL markup for critical poking with unsynchronized references;
2010-12-17 wenzelm 2010-12-17 merged
2010-12-17 haftmann 2010-12-17 avoid slightly odd Conv.tap_thy
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-12-15 haftmann 2010-12-15 simplified evaluation function names
2010-12-07 blanchet 2010-12-07 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
2010-12-06 haftmann 2010-12-06 moved bootstrap of type_lifting to Fun
2010-12-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
2010-12-03 wenzelm 2010-12-03 setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
2010-12-01 haftmann 2010-12-01 merged