src/Tools/Code/code_simp.ML
Fri, 03 Jan 2014 21:52:00 +0100 haftmann spelling
Wed, 01 Jan 2014 14:29:22 +0100 wenzelm clarified simplifier context;
Fri, 06 Sep 2013 20:55:14 +0200 haftmann tuned
Thu, 22 Aug 2013 21:15:43 +0200 haftmann separate tracing option for code_simp
Sat, 27 Jul 2013 18:02:41 +0200 haftmann more correct context for dynamic invocations of static code conversions etc.
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Tue, 05 Jun 2012 07:05:56 +0200 haftmann prefer records with speaking labels over deeply nested tuples
Thu, 19 Apr 2012 10:16:51 +0200 haftmann dropped dead code;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Fri, 01 Jul 2011 15:16:03 +0200 wenzelm proper @{binding} antiquotations (relevant for formal references);
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 18:33:35 +0100 wenzelm merged
Fri, 17 Dec 2010 18:24:44 +0100 haftmann avoid slightly odd Conv.tap_thy
Fri, 17 Dec 2010 13:45:43 +0100 wenzelm refer to regular structure Simplifier;
Thu, 16 Dec 2010 09:28:19 +0100 haftmann more uniform naming
Wed, 15 Dec 2010 09:47:12 +0100 haftmann simplified evaluation function names
Tue, 21 Sep 2010 15:46:06 +0200 haftmann no_frees_* is subsumed by new framework mechanisms in Code_Preproc
Tue, 21 Sep 2010 14:42:29 +0200 haftmann more conventional conversion signature
Fri, 17 Sep 2010 11:05:51 +0200 haftmann refined static_eval_conv_simple; tuned comments
Thu, 16 Sep 2010 16:51:34 +0200 haftmann separation of static and dynamic thy context
Thu, 26 Aug 2010 16:34:10 +0200 wenzelm simplification/standardization of some theory data;
Mon, 23 Aug 2010 11:51:32 +0200 haftmann use Code_Thingol.static_eval_conv_simple
Mon, 23 Aug 2010 11:09:49 +0200 haftmann refined and unified naming convention for dynamic code evaluation techniques
Fri, 16 Jul 2010 13:57:29 +0200 haftmann tuned interpunctation
Thu, 08 Jul 2010 16:19:24 +0200 haftmann tuned titles
Fri, 18 Jun 2010 15:26:04 +0200 haftmann code_simp: only succeed on real progress
Fri, 18 Jun 2010 15:03:21 +0200 haftmann conclude simplification with default simpset
Thu, 17 Jun 2010 15:59:47 +0200 haftmann more precise code
Thu, 17 Jun 2010 10:45:10 +0200 haftmann added simp evaluator
Tue, 15 Jun 2010 14:28:22 +0200 haftmann added code_simp infrastructure
less more (0) tip