src/HOL/HOL.thy
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
2010-12-01 haftmann 2010-12-01 file for package tool type_mapper carries the same name as its Isar command
2010-12-01 wenzelm 2010-12-01 simplified HOL.eq simproc matching;
2010-11-26 wenzelm 2010-11-26 lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;
2010-11-17 haftmann 2010-11-17 module for functorial mappers
2010-10-27 blanchet 2010-10-27 reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
2010-09-29 krauss 2010-09-29 backed out my old attempt at single_hyp_subst_tac (67cd6ed76446) It never was totally reliable, and better alternatives now exist (Subgoal.FOCUS).
2010-09-27 blanchet 2010-09-27 merged
2010-09-27 blanchet 2010-09-27 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
2010-09-27 haftmann 2010-09-27 corrected OCaml operator precedence
2010-09-20 haftmann 2010-09-20 Pure equality is a regular cpde operation
2010-09-16 haftmann 2010-09-16 adjusted to changes in Code_Runtime
2010-09-15 wenzelm 2010-09-15 dropped obsolete src/Tools/random_word.ML -- superseded by src/Tools/Metis/src/Random.sml stemming from the Metis distribution;
2010-09-15 haftmann 2010-09-15 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
2010-09-15 haftmann 2010-09-15 Code_Runtime.value, corresponding to ML_Context.value
2010-09-15 haftmann 2010-09-15 code_eval renamed to code_runtime
2010-09-15 haftmann 2010-09-15 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
2010-09-11 blanchet 2010-09-11 added Auto Try to the mix of automatic tools
2010-09-10 haftmann 2010-09-10 Haskell == is infix, not infixl
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-09-02 blanchet 2010-09-02 merged
2010-09-02 blanchet 2010-09-02 use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine
2010-09-02 haftmann 2010-09-02 merged
2010-09-02 haftmann 2010-09-02 avoid cyclic modules