src/HOL/HOL.thy
2011-10-12 ago modernized structure Induct_Tacs;
2011-09-20 ago New proof method "induction" that gives induction hypotheses the name IH.
2011-09-13 ago tuned proofs
2011-08-18 ago moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
2011-08-10 ago old term operations are legacy;
2011-08-03 ago removing the SML evaluator
2011-07-02 ago install case certificate for If after code_datatype declaration for bool
2011-06-29 ago tuned signature;
2011-06-27 ago ML antiquotations are managed as theory data, with proper name space and entity markup;
2011-05-14 ago simplified BLAST_DATA;
2011-05-14 ago modernized functor names;
2011-05-13 ago clarified map_simpset versus Simplifier.map_simpset_global;
2011-04-26 ago simplified Blast setup;
2011-04-22 ago misc tuning and simplification;
2011-04-22 ago proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
2011-04-22 ago modernized Quantifier1 simproc setup;
2011-04-22 ago clarified simpset setup;
2011-04-20 ago explicit context for Codegen.eval_term etc.;
2011-04-20 ago merged
2011-04-20 ago making the evaluation of HOL.implies lazy even in strict languages by mapping it to an if statement
2011-04-19 ago eliminated Codegen.mode in favour of explicit argument;
2011-04-16 ago modernized structure Proof_Context;
2011-04-08 ago explicit structure Syntax_Trans;
2011-03-31 ago corrected infix precedence for boolean operators in Haskell
2011-03-22 ago more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
2011-02-28 ago declare ext [intro]: Extensionality now available by default
2011-02-23 ago setup case_product attribute in HOL and FOL
2011-02-21 ago renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2011-01-27 ago CRITICAL markup for critical poking with unsynchronized references;
2010-12-17 ago merged
2010-12-17 ago avoid slightly odd Conv.tap_thy
2010-12-17 ago replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-12-15 ago simplified evaluation function names
2010-12-07 ago load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
2010-12-06 ago moved bootstrap of type_lifting to Fun
2010-12-06 ago replace `type_mapper` by the more adequate `type_lifting`
2010-12-03 ago setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
2010-12-01 ago merged
2010-12-01 ago file for package tool type_mapper carries the same name as its Isar command
2010-12-01 ago simplified HOL.eq simproc matching;
2010-11-26 ago lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;
2010-11-17 ago module for functorial mappers
2010-10-27 ago 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 ago backed out my old attempt at single_hyp_subst_tac (67cd6ed76446)
2010-09-27 ago merged
2010-09-27 ago 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 ago corrected OCaml operator precedence
2010-09-20 ago Pure equality is a regular cpde operation
2010-09-16 ago adjusted to changes in Code_Runtime
2010-09-15 ago dropped obsolete src/Tools/random_word.ML -- superseded by src/Tools/Metis/src/Random.sml stemming from the Metis distribution;
2010-09-15 ago introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
2010-09-15 ago Code_Runtime.value, corresponding to ML_Context.value
2010-09-15 ago code_eval renamed to code_runtime
2010-09-15 ago replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
2010-09-11 ago added Auto Try to the mix of automatic tools
2010-09-10 ago Haskell == is infix, not infixl
2010-09-06 ago more antiquotations;
2010-09-02 ago merged
2010-09-02 ago use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
2010-09-02 ago merged