src/HOL/HOL.thy
2017-10-22 ago derived axiom iffI as a lemma (thanks to Alexander Maletzky)
2017-10-09 ago tuned imports
2017-07-02 ago proper concept of code declaration wrt. atomicity and Isar declarations
2017-06-17 ago added simp rules
2016-09-18 ago clarified notation: iterated quantifier is negated as one chunk;
2016-09-18 ago clarified notation;
2016-08-01 ago misc tuning and modernization;
2016-07-29 ago add lemmas contributed by Peter Gammie
2016-04-12 ago Type_Infer.object_logic controls improvement of type inference result;
2016-04-08 ago eliminated unused simproc identifier;
2016-03-05 ago abbreviations for \<nexists>;
2016-03-05 ago old HOL syntax is for input only;
2016-02-23 ago more canonical names
2016-01-12 ago eliminated old defs;
2015-12-28 ago former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-27 ago discontinued ASCII replacement syntax <->;
2015-12-22 ago stripped some legacy
2015-12-07 ago isabelle update_cartouches -c -t;
2015-10-09 ago discontinued specific HTML syntax;
2015-09-21 ago isabelle update_cartouches;
2015-09-21 ago Added new simplifier predicate ASSUMPTION
2015-09-13 ago tuned proofs -- less legacy;
2015-09-09 ago simplified simproc programming interfaces;
2015-09-01 ago eliminated \<Colon>;
2015-07-25 ago updated to infer_instantiate;
2015-07-20 ago proper LaTeX;
2015-07-19 ago more symbols;
2015-07-18 ago isabelle update_cartouches;
2015-05-09 ago undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
2015-05-03 ago swap False to the right in assumptions to be eliminated at the right end
2015-04-28 ago undid 6d7b7a037e8d
2015-04-25 ago new ==> simp rule
2015-04-22 ago added simp rules for ==>
2015-04-09 ago clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-08 ago proper context for Object_Logic operations;
2015-04-06 ago local setup of induction tools, with restricted access to auxiliary consts;
2015-04-06 ago tuned;
2015-03-31 ago added lemmas
2015-03-23 ago fix parameter order of NO_MATCH
2015-03-06 ago clarified context;
2015-03-06 ago Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 ago clarified signature;
2015-03-04 ago tuned signature -- prefer qualified names;
2015-02-11 ago Merge
2015-02-10 ago New lemmas and a bit of tidying up.
2015-02-10 ago misc tuning;
2015-02-10 ago proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
2014-11-22 ago named_theorems: multiple args;
2014-11-10 ago proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 ago proper context;
2014-11-09 ago proper context for match_tac etc.;
2014-11-09 ago proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-02 ago modernized header uniformly as section;
2014-10-30 ago eliminated aliases;
2014-10-30 ago disable coercions for NO_MATCH
2014-10-29 ago modernized setup;
2014-10-24 ago move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
2014-10-13 ago Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
2014-08-16 ago updated to named_theorems;
2014-08-16 ago updated to named_theorems;