| Thu, 16 Sep 2010 16:51:34 +0200 |
haftmann |
separation of static and dynamic thy context
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 15:11:39 +0200 |
haftmann |
ignore code cache optionally; corrected scope of term value in static_eval_conv
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 19:47:40 +0200 |
wenzelm |
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 15:01:13 +0200 |
haftmann |
repaired attribute code_unfold_post which has ever been broken
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:57:22 +0200 |
haftmann |
dropped pre_post_conv
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:51:32 +0200 |
haftmann |
added static_eval_conv
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:09:49 +0200 |
haftmann |
refined and unified naming convention for dynamic code evaluation techniques
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 13:43:01 +0200 |
haftmann |
minimize sorts in certificate instantiation
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Tue, 15 Jun 2010 14:28:22 +0200 |
haftmann |
added code_simp infrastructure
|
file |
diff |
annotate
|
| Mon, 07 Jun 2010 13:42:38 +0200 |
haftmann |
more consistent naming aroud type classes and instances
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 13:08:14 +0200 |
wenzelm |
of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 17:03:53 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 16:11:45 +0100 |
wenzelm |
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 11:06:20 +0100 |
haftmann |
simplified
|
file |
diff |
annotate
|
| Wed, 13 Jan 2010 12:20:37 +0100 |
haftmann |
explicit abstract type of code certificates
|
file |
diff |
annotate
|
| Wed, 13 Jan 2010 10:18:45 +0100 |
haftmann |
function transformer preprocessor applies to both code generators
|
file |
diff |
annotate
|
| Tue, 12 Jan 2010 16:27:42 +0100 |
haftmann |
code certificates as integral part of code generation
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 16:00:24 +0100 |
haftmann |
code cache only persists on equal theories
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 14:09:56 +0100 |
haftmann |
code cache without copy; tuned
|
file |
diff |
annotate
|
| Wed, 23 Dec 2009 08:31:15 +0100 |
haftmann |
reduced code generator cache to the baremost minimum
|
file |
diff |
annotate
|
| Wed, 02 Dec 2009 17:53:35 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 15 Nov 2009 19:44:29 +0100 |
wenzelm |
permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 13:48:06 +0200 |
haftmann |
map_range (and map_index) combinator
|
file |
diff |
annotate
|
| Mon, 05 Oct 2009 15:04:45 +0200 |
haftmann |
tuned handling of type variable names further
|
file |
diff |
annotate
|
| Mon, 05 Oct 2009 08:36:33 +0200 |
haftmann |
variables in type schemes must be renamed simultaneously with variables in equations
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 23:30:37 +0200 |
wenzelm |
Sorts.of_sort_derivation: no pp here;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2009 11:31:20 +0200 |
haftmann |
moved eq handling in nbe into separate oracle
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 12:24:49 +0200 |
haftmann |
moved all technical processing of code equations to code_thingol.ML
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 08:37:37 +0200 |
haftmann |
attempt to move desymbolization to translation
|
file |
diff |
annotate
|
| Fri, 31 Jul 2009 10:49:09 +0200 |
haftmann |
added a somehow clueless comment
|
file |
diff |
annotate
|
| Fri, 31 Jul 2009 09:34:05 +0200 |
haftmann |
cleaned up variable desymbolification and argument expansion
|
file |
diff |
annotate
|
| Wed, 22 Jul 2009 11:23:09 +0200 |
wenzelm |
merged, resolving trivial conflict;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 15:44:31 +0200 |
haftmann |
integrated add_triv_classes into evaluation stack
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 16:27:34 +0200 |
haftmann |
added code_unfold_post attribute
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:01:41 +0200 |
wenzelm |
renamed functor TableFun to Table, and GraphFun to Graph;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2009 08:18:07 +0200 |
haftmann |
tuned structure Code internally
|
file |
diff |
annotate
|
| Tue, 07 Jul 2009 17:21:27 +0200 |
haftmann |
tuned interface of structure Code
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
| base
|