src/Tools/Code/code_preproc.ML
Mon, 22 Oct 2012 19:02:36 +0200 haftmann close code theorems explicitly after preprocessing
Tue, 05 Jun 2012 10:12:54 +0200 haftmann apply preprocessing simpset also to rhs of abstract code equations
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
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;
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
Fri, 21 Oct 2011 11:17:12 +0200 bulwahn removing redundant attribute code_inline in the code generator
Wed, 19 Oct 2011 09:11:19 +0200 bulwahn removing declaration of code_unfold to address the old code generator
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;
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
Mon, 18 Apr 2011 13:26:39 +0200 wenzelm pass plain Proof.context for pretty printing;
Mon, 18 Apr 2011 11:13:29 +0200 wenzelm simplified pretty printing context, which is only required for certain kernel operations;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Tue, 21 Dec 2010 09:18:29 +0100 haftmann canonical handling of theory context argument
Fri, 17 Dec 2010 14:09:37 +0100 wenzelm clarified exports of structure Simplifier;
Thu, 16 Dec 2010 09:40:15 +0100 haftmann more appropriate closures for static evaluation
Wed, 15 Dec 2010 09:47:12 +0100 haftmann simplified evaluation function names
Tue, 26 Oct 2010 12:19:22 +0200 haftmann tuned
Tue, 26 Oct 2010 12:15:55 +0200 haftmann dropped accidental doubled computation
Tue, 21 Sep 2010 15:46:05 +0200 haftmann avoid frees and vars in terms to be evaluated by abstracting and applying
Thu, 16 Sep 2010 16:51:34 +0200 haftmann separation of static and dynamic thy context
Wed, 15 Sep 2010 15:11:39 +0200 haftmann ignore code cache optionally; corrected scope of term value in static_eval_conv
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;
Wed, 01 Sep 2010 15:01:13 +0200 haftmann repaired attribute code_unfold_post which has ever been broken
Mon, 23 Aug 2010 11:57:22 +0200 haftmann dropped pre_post_conv
Mon, 23 Aug 2010 11:51:32 +0200 haftmann added static_eval_conv
Mon, 23 Aug 2010 11:09:49 +0200 haftmann refined and unified naming convention for dynamic code evaluation techniques
Mon, 09 Aug 2010 13:43:01 +0200 haftmann minimize sorts in certificate instantiation
Thu, 08 Jul 2010 16:19:24 +0200 haftmann tuned titles
Tue, 15 Jun 2010 14:28:22 +0200 haftmann added code_simp infrastructure
Mon, 07 Jun 2010 13:42:38 +0200 haftmann more consistent naming aroud type classes and instances
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
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;
Sun, 11 Apr 2010 13:08:14 +0200 wenzelm of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
Sun, 07 Mar 2010 11:57:16 +0100 wenzelm modernized structure Local_Defs;
Fri, 19 Feb 2010 17:03:53 +0100 wenzelm merged
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;
Fri, 19 Feb 2010 11:06:20 +0100 haftmann simplified
Wed, 13 Jan 2010 12:20:37 +0100 haftmann explicit abstract type of code certificates
Wed, 13 Jan 2010 10:18:45 +0100 haftmann function transformer preprocessor applies to both code generators
Tue, 12 Jan 2010 16:27:42 +0100 haftmann code certificates as integral part of code generation
Mon, 04 Jan 2010 16:00:24 +0100 haftmann code cache only persists on equal theories
Mon, 04 Jan 2010 14:09:56 +0100 haftmann code cache without copy; tuned
Wed, 23 Dec 2009 08:31:15 +0100 haftmann reduced code generator cache to the baremost minimum
Wed, 02 Dec 2009 17:53:35 +0100 haftmann tuned
Sun, 15 Nov 2009 19:44:29 +0100 wenzelm permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Thu, 22 Oct 2009 13:48:06 +0200 haftmann map_range (and map_index) combinator
Mon, 05 Oct 2009 15:04:45 +0200 haftmann tuned handling of type variable names further
Mon, 05 Oct 2009 08:36:33 +0200 haftmann variables in type schemes must be renamed simultaneously with variables in equations
Wed, 30 Sep 2009 23:30:37 +0200 wenzelm Sorts.of_sort_derivation: no pp here;
Wed, 09 Sep 2009 11:31:20 +0200 haftmann moved eq handling in nbe into separate oracle
Mon, 10 Aug 2009 12:24:49 +0200 haftmann moved all technical processing of code equations to code_thingol.ML
Mon, 10 Aug 2009 08:37:37 +0200 haftmann attempt to move desymbolization to translation
Fri, 31 Jul 2009 10:49:09 +0200 haftmann added a somehow clueless comment
Fri, 31 Jul 2009 09:34:05 +0200 haftmann cleaned up variable desymbolification and argument expansion
Wed, 22 Jul 2009 11:23:09 +0200 wenzelm merged, resolving trivial conflict;
Tue, 21 Jul 2009 15:44:31 +0200 haftmann integrated add_triv_classes into evaluation stack
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.;
Tue, 14 Jul 2009 16:27:34 +0200 haftmann added code_unfold_post attribute
less more (0) -60 tip