src/HOL/HOL.thy
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;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-08-16 wenzelm 2014-08-16 modernized module name and setup;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-05-12 wenzelm 2014-05-12 tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
2014-04-03 blanchet 2014-04-03 use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
2014-02-26 haftmann 2014-02-26 prefer proof context over background theory
2014-02-20 wenzelm 2014-02-20 modernized tool setup; tuned;
2014-02-10 wenzelm 2014-02-10 discontinued axiomatic 'classes', 'classrel', 'arities';
2014-02-10 wenzelm 2014-02-10 more explicit axiomatization;
2014-02-01 wenzelm 2014-02-01 more standard file/module names;
2014-01-01 haftmann 2014-01-01 fundamental treatment of undefined vs. universally partial replaces code_abort
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-08-22 haftmann 2013-08-22 congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj