src/Tools/Code/code_preproc.ML
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 10 Apr 2013 15:30:19 +0200 wenzelm more standard module name Axclass (according to file name);
Tue, 09 Apr 2013 15:29:25 +0200 wenzelm discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
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;
less more (0) -15 tip