| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
optional timing for code generator conversions
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
corrected closure scope of static_conv_thingol;
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified names of variants
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:52:14 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Fri, 09 Jan 2015 08:36:59 +0100 |
haftmann |
modernized and more uniform style
|
file |
diff |
annotate
|
| Thu, 15 May 2014 16:38:31 +0200 |
haftmann |
syntactic means to prevent accidental mixup of static and dynamic context
|
file |
diff |
annotate
|
| Thu, 15 May 2014 16:38:29 +0200 |
haftmann |
dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
|
file |
diff |
annotate
|
| Fri, 09 May 2014 08:13:36 +0200 |
haftmann |
dimiss simplified as evaluator due to little practical relevance
|
file |
diff |
annotate
|
| Fri, 09 May 2014 08:13:26 +0200 |
haftmann |
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
|
file |
diff |
annotate
|
| Thu, 01 May 2014 09:30:33 +0200 |
haftmann |
cleanup
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 11:57:52 +0100 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 23:50:49 +0100 |
haftmann |
prefer explicit code symbol type over ad-hoc name mangling
|
file |
diff |
annotate
|
| Fri, 03 Jan 2014 22:04:44 +0100 |
haftmann |
proper context for simplifier invocations in code generation stack
|
file |
diff |
annotate
|
| Fri, 03 Jan 2014 21:52:00 +0100 |
haftmann |
spelling
|
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
|
| Thu, 22 Aug 2013 21:15:43 +0200 |
haftmann |
separate tracing option for code_simp
|
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
|
| Tue, 05 Jun 2012 07:05:56 +0200 |
haftmann |
prefer records with speaking labels over deeply nested tuples
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 10:16:51 +0200 |
haftmann |
dropped dead code;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:16:03 +0200 |
wenzelm |
proper @{binding} antiquotations (relevant for formal references);
|
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 18:33:35 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 18:24:44 +0100 |
haftmann |
avoid slightly odd Conv.tap_thy
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 13:45:43 +0100 |
wenzelm |
refer to regular structure Simplifier;
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 09:28:19 +0100 |
haftmann |
more uniform naming
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 09:47:12 +0100 |
haftmann |
simplified evaluation function names
|
file |
diff |
annotate
|
| Tue, 21 Sep 2010 15:46:06 +0200 |
haftmann |
no_frees_* is subsumed by new framework mechanisms in Code_Preproc
|
file |
diff |
annotate
|
| Tue, 21 Sep 2010 14:42:29 +0200 |
haftmann |
more conventional conversion signature
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 11:05:51 +0200 |
haftmann |
refined static_eval_conv_simple; tuned comments
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 16:51:34 +0200 |
haftmann |
separation of static and dynamic thy context
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 16:34:10 +0200 |
wenzelm |
simplification/standardization of some theory data;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:51:32 +0200 |
haftmann |
use Code_Thingol.static_eval_conv_simple
|
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
|
| Fri, 16 Jul 2010 13:57:29 +0200 |
haftmann |
tuned interpunctation
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Fri, 18 Jun 2010 15:26:04 +0200 |
haftmann |
code_simp: only succeed on real progress
|
file |
diff |
annotate
|
| Fri, 18 Jun 2010 15:03:21 +0200 |
haftmann |
conclude simplification with default simpset
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 15:59:47 +0200 |
haftmann |
more precise code
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 10:45:10 +0200 |
haftmann |
added simp evaluator
|
file |
diff |
annotate
|
| Tue, 15 Jun 2010 14:28:22 +0200 |
haftmann |
added code_simp infrastructure
|
file |
diff |
annotate
|