Mon, 26 Apr 2010 09:45:22 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 09:26:31 -0700 |
huffman |
syntax precedence for If and Let
|
file |
diff |
annotate
|
Sun, 25 Apr 2010 23:09:32 +0200 |
wenzelm |
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
|
file |
diff |
annotate
|
Fri, 23 Apr 2010 19:36:04 +0200 |
wenzelm |
removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;
|
file |
diff |
annotate
|
Wed, 21 Apr 2010 12:10:52 +0200 |
bulwahn |
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
|
file |
diff |
annotate
|
Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
Mon, 29 Mar 2010 14:49:53 +0200 |
blanchet |
reintroduce efficient set structure to collect "no_atp" theorems
|
file |
diff |
annotate
|
Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
Wed, 17 Mar 2010 12:01:01 +0100 |
blanchet |
fix typo in "nitpick_choice_spec" attribute name (singular, not plural)
|
file |
diff |
annotate
|
Wed, 17 Mar 2010 09:14:43 +0100 |
blanchet |
added support for "specification" and "ax_specification" constructs to Nitpick
|
file |
diff |
annotate
|
Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
Mon, 01 Mar 2010 13:42:31 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
Fri, 26 Feb 2010 21:43:26 +0100 |
wenzelm |
tuned hyp_subst_tac';
|
file |
diff |
annotate
|
Thu, 25 Feb 2010 22:32:09 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
Sun, 31 Jan 2010 15:22:40 +0100 |
berghofe |
merged
|
file |
diff |
annotate
|
Sat, 30 Jan 2010 16:59:49 +0100 |
berghofe |
Added setup for simplification of equality constraints in cases rules.
|
file |
diff |
annotate
|
Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
Fri, 15 Jan 2010 14:43:00 +0100 |
berghofe |
merged
|
file |
diff |
annotate
|
Sun, 10 Jan 2010 18:03:20 +0100 |
berghofe |
Added setup for simplification of equality constraints in induction rules.
|
file |
diff |
annotate
|
Wed, 13 Jan 2010 08:56:15 +0100 |
haftmann |
some syntax setup for Scala
|
file |
diff |
annotate
|
Mon, 11 Jan 2010 16:45:02 +0100 |
haftmann |
tuned code equations
|
file |
diff |
annotate
|
Fri, 08 Jan 2010 14:34:17 +0100 |
haftmann |
boolean operators for scala
|
file |
diff |
annotate
|
Fri, 08 Jan 2010 12:25:15 +0100 |
haftmann |
a primitive scala serializer
|
file |
diff |
annotate
|
Wed, 30 Dec 2009 10:24:53 +0100 |
krauss |
killed a few warnings
|
file |
diff |
annotate
|
Mon, 07 Dec 2009 16:27:48 +0100 |
haftmann |
split off evaluation mechanisms in separte module Code_Eval
|
file |
diff |
annotate
|
Tue, 24 Nov 2009 17:19:33 +0100 |
wenzelm |
some rearangement of load order to keep preferences adjacent -- slightly fragile;
|
file |
diff |
annotate
|
Thu, 19 Nov 2009 08:25:57 +0100 |
bulwahn |
replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
|
file |
diff |
annotate
|
Tue, 10 Nov 2009 15:33:35 +0100 |
wenzelm |
removed unused Quickcheck_RecFun_Simps;
|
file |
diff |
annotate
|
Sun, 08 Nov 2009 19:15:37 +0100 |
wenzelm |
modernized structure Reorient_Proc;
|
file |
diff |
annotate
|
Sun, 01 Nov 2009 15:44:26 +0100 |
wenzelm |
modernized structure Context_Rules;
|
file |
diff |
annotate
|
Fri, 30 Oct 2009 18:32:40 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 16:59:12 +0100 |
wenzelm |
modernized some structure names;
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 16:06:15 +0100 |
wenzelm |
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 10:51:41 +0100 |
haftmann |
tuned code setup for primitive boolean connectors
|
file |
diff |
annotate
|
Fri, 23 Oct 2009 17:12:36 +0200 |
haftmann |
turned off old quickcheck
|
file |
diff |
annotate
|
Wed, 21 Oct 2009 17:34:35 +0200 |
blanchet |
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 15:02:48 +0100 |
paulson |
Removal of the unused atpset concept, the atp attribute and some related code.
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
Mon, 28 Sep 2009 23:13:37 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added first prototype of the extended predicate compiler
|
file |
diff |
annotate
|
Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
experimenting to add some useful interface for definitions
|
file |
diff |
annotate
|
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
|
file |
diff |
annotate
|
Wed, 09 Sep 2009 11:31:20 +0200 |
haftmann |
moved eq handling in nbe into separate oracle
|
file |
diff |
annotate
|
Wed, 26 Aug 2009 11:40:28 +0200 |
boehmes |
added further conversions and conversionals
|
file |
diff |
annotate
|
Fri, 24 Jul 2009 21:21:45 +0200 |
wenzelm |
renamed functor BlastFun to Blast, require explicit theory;
|
file |
diff |
annotate
|
Fri, 24 Jul 2009 18:58:58 +0200 |
wenzelm |
renamed functor ProjectRuleFun to Project_Rule;
|
file |
diff |
annotate
|
Fri, 24 Jul 2009 12:33:00 +0200 |
wenzelm |
renamed functor InductFun to Induct;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Tue, 21 Jul 2009 14:36:26 +0200 |
haftmann |
moved abstract algebra section to the end
|
file |
diff |
annotate
|
Tue, 14 Jul 2009 16:27:31 +0200 |
haftmann |
tuned code annotations
|
file |
diff |
annotate
|
Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
Tue, 07 Jul 2009 17:21:26 +0200 |
haftmann |
more accurate certificates for constant aliasses
|
file |
diff |
annotate
|
Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
Thu, 25 Jun 2009 14:59:29 +0200 |
haftmann |
arbitrary farewell
|
file |
diff |
annotate
|
Sat, 30 May 2009 12:52:57 +0200 |
wenzelm |
modernized method setup;
|
file |
diff |
annotate
|
Sat, 16 May 2009 15:24:35 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
Sat, 16 May 2009 15:23:52 +0200 |
bulwahn |
added collection of simplification rules of recursive functions for quickcheck
|
file |
diff |
annotate
|