src/HOL/HOL.thy
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Mon, 01 Mar 2010 13:42:31 +0100 haftmann merged
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Fri, 26 Feb 2010 21:43:26 +0100 wenzelm tuned hyp_subst_tac';
Thu, 25 Feb 2010 22:32:09 +0100 wenzelm more antiquotations;
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Sun, 31 Jan 2010 15:22:40 +0100 berghofe merged
Sat, 30 Jan 2010 16:59:49 +0100 berghofe Added setup for simplification of equality constraints in cases rules.
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Fri, 15 Jan 2010 14:43:00 +0100 berghofe merged
Sun, 10 Jan 2010 18:03:20 +0100 berghofe Added setup for simplification of equality constraints in induction rules.
Wed, 13 Jan 2010 08:56:15 +0100 haftmann some syntax setup for Scala
Mon, 11 Jan 2010 16:45:02 +0100 haftmann tuned code equations
Fri, 08 Jan 2010 14:34:17 +0100 haftmann boolean operators for scala
Fri, 08 Jan 2010 12:25:15 +0100 haftmann a primitive scala serializer
Wed, 30 Dec 2009 10:24:53 +0100 krauss killed a few warnings
Mon, 07 Dec 2009 16:27:48 +0100 haftmann split off evaluation mechanisms in separte module Code_Eval
Tue, 24 Nov 2009 17:19:33 +0100 wenzelm some rearangement of load order to keep preferences adjacent -- slightly fragile;
Thu, 19 Nov 2009 08:25:57 +0100 bulwahn replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
Tue, 10 Nov 2009 15:33:35 +0100 wenzelm removed unused Quickcheck_RecFun_Simps;
Sun, 08 Nov 2009 19:15:37 +0100 wenzelm modernized structure Reorient_Proc;
Sun, 01 Nov 2009 15:44:26 +0100 wenzelm modernized structure Context_Rules;
Fri, 30 Oct 2009 18:32:40 +0100 haftmann tuned code setup
Thu, 29 Oct 2009 16:59:12 +0100 wenzelm modernized some structure names;
Thu, 29 Oct 2009 16:06:15 +0100 wenzelm separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
Mon, 26 Oct 2009 10:51:41 +0100 haftmann tuned code setup for primitive boolean connectors
Fri, 23 Oct 2009 17:12:36 +0200 haftmann turned off old quickcheck
Wed, 21 Oct 2009 17:34:35 +0200 blanchet renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
Tue, 20 Oct 2009 15:02:48 +0100 paulson Removal of the unused atpset concept, the atp attribute and some related code.
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Mon, 28 Sep 2009 23:13:37 +0200 wenzelm misc tuning and modernization;
Mon, 28 Sep 2009 22:47:34 +0200 wenzelm moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
Wed, 23 Sep 2009 16:20:12 +0200 bulwahn added first prototype of the extended predicate compiler
Wed, 23 Sep 2009 16:20:12 +0200 bulwahn experimenting to add some useful interface for definitions
Wed, 23 Sep 2009 16:20:12 +0200 bulwahn added predicate compile preprocessing structure for definitional thms -- probably is replaced by hooking the theorem command differently
Wed, 09 Sep 2009 11:31:20 +0200 haftmann moved eq handling in nbe into separate oracle
Wed, 26 Aug 2009 11:40:28 +0200 boehmes added further conversions and conversionals
Fri, 24 Jul 2009 21:21:45 +0200 wenzelm renamed functor BlastFun to Blast, require explicit theory;
Fri, 24 Jul 2009 18:58:58 +0200 wenzelm renamed functor ProjectRuleFun to Project_Rule;
Fri, 24 Jul 2009 12:33:00 +0200 wenzelm renamed functor InductFun to Induct;
Thu, 23 Jul 2009 18:44:09 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
Tue, 21 Jul 2009 14:36:26 +0200 haftmann moved abstract algebra section to the end
Tue, 14 Jul 2009 16:27:31 +0200 haftmann tuned code annotations
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Tue, 07 Jul 2009 17:21:26 +0200 haftmann more accurate certificates for constant aliasses
Thu, 02 Jul 2009 17:34:14 +0200 wenzelm renamed NamedThmsFun to Named_Thms;
Thu, 25 Jun 2009 14:59:29 +0200 haftmann arbitrary farewell
Sat, 30 May 2009 12:52:57 +0200 wenzelm modernized method setup;
Sat, 16 May 2009 15:24:35 +0200 bulwahn merged
Sat, 16 May 2009 15:23:52 +0200 bulwahn added collection of simplification rules of recursive functions for quickcheck
Sat, 16 May 2009 11:28:02 +0200 nipkow "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
Thu, 14 May 2009 15:09:48 +0200 haftmann merged module code_unit.ML into code.ML
Thu, 14 May 2009 09:16:34 +0200 haftmann rewrite op = == eq handled by simproc
Wed, 13 May 2009 18:41:35 +0200 haftmann itself is instance of eq
Tue, 12 May 2009 19:30:33 +0200 haftmann transferred code generator preprocessor into separate module
Wed, 29 Apr 2009 17:15:01 -0700 huffman reimplement reorientation simproc using theory data
Sat, 25 Apr 2009 21:28:04 +0200 wenzelm misc cleanup of auto_solve and quickcheck:
Fri, 24 Apr 2009 08:24:54 +0200 haftmann generic postprocessing scheme for term evaluations
Thu, 23 Apr 2009 12:17:50 +0200 haftmann avoid local [code]
Fri, 17 Apr 2009 14:29:56 +0200 haftmann re-engineering of evaluation conversions
less more (0) -300 -100 -60 tip