src/HOL/HOL.thy
Thu, 30 Oct 2014 09:15:54 +0100 hoelzl disable coercions for NO_MATCH
Wed, 29 Oct 2014 19:01:49 +0100 wenzelm modernized setup;
Fri, 24 Oct 2014 15:07:49 +0200 hoelzl move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
Mon, 13 Oct 2014 18:45:48 +0200 wenzelm Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
Sat, 16 Aug 2014 22:14:57 +0200 wenzelm updated to named_theorems;
Sat, 16 Aug 2014 21:11:08 +0200 wenzelm updated to named_theorems;
Sat, 16 Aug 2014 20:46:59 +0200 wenzelm updated to named_theorems;
Sat, 16 Aug 2014 13:23:50 +0200 wenzelm modernized module name and setup;
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Mon, 12 May 2014 17:17:32 +0200 wenzelm tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
Thu, 03 Apr 2014 10:51:22 +0200 blanchet 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
Wed, 26 Feb 2014 11:57:52 +0100 haftmann prefer proof context over background theory
Thu, 20 Feb 2014 20:19:41 +0100 wenzelm modernized tool setup;
Mon, 10 Feb 2014 22:08:18 +0100 wenzelm discontinued axiomatic 'classes', 'classrel', 'arities';
Mon, 10 Feb 2014 21:03:28 +0100 wenzelm more explicit axiomatization;
Sat, 01 Feb 2014 21:09:53 +0100 wenzelm more standard file/module names;
Wed, 01 Jan 2014 01:05:48 +0100 haftmann fundamental treatment of undefined vs. universally partial replaces code_abort
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Thu, 22 Aug 2013 21:15:43 +0200 haftmann congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj
Sun, 14 Jul 2013 00:08:15 +0200 wenzelm recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;
Sat, 13 Jul 2013 00:50:49 +0200 wenzelm hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Sun, 23 Jun 2013 22:31:50 +0200 wenzelm tuned message -- more markup;
Thu, 30 May 2013 12:35:40 +0200 wenzelm standardized aliases;
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Sat, 27 Apr 2013 20:50:20 +0200 wenzelm uniform Proof.context for hyp_subst_tac;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 10 Apr 2013 21:20:35 +0200 wenzelm tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
Wed, 10 Apr 2013 19:14:47 +0200 wenzelm merged
Wed, 10 Apr 2013 17:17:16 +0200 wenzelm discontinued obsolete ML antiquotation @{claset};
Tue, 22 Jan 2013 14:33:45 +0100 traytel separate data used for case translation from the datatype package
Thu, 28 Feb 2013 16:54:52 +0100 wenzelm just one HOLogic.Trueprop_conv, with regular exception CTERM;
Thu, 28 Feb 2013 13:24:51 +0100 wenzelm marginalized historic strip_tac;
Wed, 06 Feb 2013 17:18:01 +0100 hoelzl check alpha equality after applying beta and eta conversion in let-simproc, otherwise the simplifier may loop
Wed, 05 Dec 2012 11:05:23 +0100 nipkow \<noteq> now has the same associativity as ~= and =
Wed, 12 Sep 2012 22:00:29 +0200 wenzelm eliminated some old material that is unused in the visible universe;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Sat, 11 Aug 2012 22:17:46 +0200 wenzelm faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
Thu, 05 Jul 2012 16:58:03 +0200 wenzelm removed obsolete rev_contrapos (cf. 1d195de59497);
Tue, 05 Jun 2012 07:10:51 +0200 haftmann prefer sys.error over plain error in Scala to avoid deprecation warning
Thu, 19 Apr 2012 19:36:24 +0200 haftmann moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
Fri, 16 Mar 2012 22:31:19 +0100 wenzelm modernized axiomatization;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Wed, 11 Jan 2012 21:04:22 +0100 wenzelm more conventional eval_tac vs. method_setup "eval";
Mon, 09 Jan 2012 18:29:42 +0100 wenzelm prefer antiquotations;
Thu, 05 Jan 2012 18:18:39 +0100 wenzelm improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
Sun, 27 Nov 2011 23:10:19 +0100 wenzelm more antiquotations;
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Sun, 20 Nov 2011 21:07:10 +0100 wenzelm eliminated obsolete "standard";
Fri, 28 Oct 2011 23:41:16 +0200 wenzelm tuned Named_Thms: proper binding;
Fri, 21 Oct 2011 11:17:14 +0200 bulwahn replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
Wed, 19 Oct 2011 08:37:16 +0200 bulwahn removing old code generator setup in the HOL theory
Wed, 12 Oct 2011 22:48:23 +0200 wenzelm modernized structure Induct_Tacs;
Tue, 20 Sep 2011 05:47:11 +0200 nipkow New proof method "induction" that gives induction hypotheses the name IH.
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Thu, 18 Aug 2011 13:25:17 +0200 haftmann moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Wed, 03 Aug 2011 13:59:59 +0200 bulwahn removing the SML evaluator
Sat, 02 Jul 2011 22:55:58 +0200 haftmann install case certificate for If after code_datatype declaration for bool
less more (0) -300 -100 -60 tip