| 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
|
| 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 {}"
|
file |
diff |
annotate
|
| Thu, 14 May 2009 15:09:48 +0200 |
haftmann |
merged module code_unit.ML into code.ML
|
file |
diff |
annotate
|
| Thu, 14 May 2009 09:16:34 +0200 |
haftmann |
rewrite op = == eq handled by simproc
|
file |
diff |
annotate
|
| Wed, 13 May 2009 18:41:35 +0200 |
haftmann |
itself is instance of eq
|
file |
diff |
annotate
|
| Tue, 12 May 2009 19:30:33 +0200 |
haftmann |
transferred code generator preprocessor into separate module
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 17:15:01 -0700 |
huffman |
reimplement reorientation simproc using theory data
|
file |
diff |
annotate
|
| Sat, 25 Apr 2009 21:28:04 +0200 |
wenzelm |
misc cleanup of auto_solve and quickcheck:
|
file |
diff |
annotate
|
| Fri, 24 Apr 2009 08:24:54 +0200 |
haftmann |
generic postprocessing scheme for term evaluations
|
file |
diff |
annotate
|
| Thu, 23 Apr 2009 12:17:50 +0200 |
haftmann |
avoid local [code]
|
file |
diff |
annotate
|
| Fri, 17 Apr 2009 14:29:56 +0200 |
haftmann |
re-engineering of evaluation conversions
|
file |
diff |
annotate
|