src/HOL/HOL.thy
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
2013-07-14 wenzelm 2013-07-14 recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;
2013-07-13 wenzelm 2013-07-13 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-23 wenzelm 2013-06-23 tuned message -- more markup;
2013-05-30 wenzelm 2013-05-30 standardized aliases;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 wenzelm 2013-04-10 tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side; declare command "print_case_translations" where it is actually defined;
2013-04-10 wenzelm 2013-04-10 merged
2013-04-10 wenzelm 2013-04-10 discontinued obsolete ML antiquotation @{claset};