| Wed, 26 Feb 2014 11:57:52 +0100 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
| Sun, 09 Feb 2014 15:26:33 +0100 |
haftmann |
build up preprocessing context only once
|
file |
diff |
annotate
|
| Fri, 03 Jan 2014 22:04:44 +0100 |
haftmann |
proper context for simplifier invocations in code generation stack
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 14:29:22 +0100 |
wenzelm |
clarified simplifier context;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2013 20:55:14 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 18:02:41 +0200 |
haftmann |
more correct context for dynamic invocations of static code conversions etc.
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 15:30:19 +0200 |
wenzelm |
more standard module name Axclass (according to file name);
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 15:29:25 +0200 |
wenzelm |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
|
file |
diff |
annotate
|
| Mon, 22 Oct 2012 19:02:36 +0200 |
haftmann |
close code theorems explicitly after preprocessing
|
file |
diff |
annotate
|
| Tue, 05 Jun 2012 10:12:54 +0200 |
haftmann |
apply preprocessing simpset also to rhs of abstract code equations
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:54 +0100 |
haftmann |
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
|
file |
diff |
annotate
|
| Fri, 21 Oct 2011 11:17:12 +0200 |
bulwahn |
removing redundant attribute code_inline in the code generator
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 09:11:19 +0200 |
bulwahn |
removing declaration of code_unfold to address the old code generator
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 23:35:30 +0200 |
wenzelm |
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 08:07:27 +0200 |
bulwahn |
code preprocessor applies simplifier when schematic variables are fixed to free variables to allow rewriting with congruence rules in the preprocessing steps
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 13:26:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:13:29 +0200 |
wenzelm |
simplified pretty printing context, which is only required for certain kernel operations;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 09:18:29 +0100 |
haftmann |
canonical handling of theory context argument
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 14:09:37 +0100 |
wenzelm |
clarified exports of structure Simplifier;
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 09:40:15 +0100 |
haftmann |
more appropriate closures for static evaluation
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 09:47:12 +0100 |
haftmann |
simplified evaluation function names
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 12:19:22 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 12:15:55 +0200 |
haftmann |
dropped accidental doubled computation
|
file |
diff |
annotate
|
| Tue, 21 Sep 2010 15:46:05 +0200 |
haftmann |
avoid frees and vars in terms to be evaluated by abstracting and applying
|
file |
diff |
annotate
|
| 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
|