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