src/HOL/HOL.thy
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
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;