2021-10-20 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
2019-01-04 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
2016-05-26 |
haftmann |
optional timing for code generator conversions
|
file |
diff |
annotate
|
2016-05-26 |
haftmann |
corrected closure scope of static_conv_thingol;
|
file |
diff |
annotate
|
2016-05-26 |
haftmann |
clarified names of variants
|
file |
diff |
annotate
|
2015-03-06 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
2015-03-06 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
2015-01-09 |
haftmann |
modernized and more uniform style
|
file |
diff |
annotate
|
2014-05-15 |
haftmann |
syntactic means to prevent accidental mixup of static and dynamic context
|
file |
diff |
annotate
|
2014-05-15 |
haftmann |
dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
|
file |
diff |
annotate
|
2014-05-09 |
haftmann |
dimiss simplified as evaluator due to little practical relevance
|
file |
diff |
annotate
|
2014-05-09 |
haftmann |
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
|
file |
diff |
annotate
|
2014-05-01 |
haftmann |
cleanup
|
file |
diff |
annotate
|
2014-02-26 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
2014-01-25 |
haftmann |
prefer explicit code symbol type over ad-hoc name mangling
|
file |
diff |
annotate
|
2014-01-03 |
haftmann |
proper context for simplifier invocations in code generation stack
|
file |
diff |
annotate
|
2014-01-03 |
haftmann |
spelling
|
file |
diff |
annotate
|
2014-01-01 |
wenzelm |
clarified simplifier context;
|
file |
diff |
annotate
|
2013-09-06 |
haftmann |
tuned
|
file |
diff |
annotate
|
2013-08-22 |
haftmann |
separate tracing option for code_simp
|
file |
diff |
annotate
|
2013-07-27 |
haftmann |
more correct context for dynamic invocations of static code conversions etc.
|
file |
diff |
annotate
|
2013-04-18 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
2012-06-05 |
haftmann |
prefer records with speaking labels over deeply nested tuples
|
file |
diff |
annotate
|
2012-04-19 |
haftmann |
dropped dead code;
|
file |
diff |
annotate
|
2011-11-23 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
2011-07-01 |
wenzelm |
proper @{binding} antiquotations (relevant for formal references);
|
file |
diff |
annotate
|
2011-04-16 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
2010-12-21 |
haftmann |
canonical handling of theory context argument
|
file |
diff |
annotate
|
2010-12-17 |
wenzelm |
merged
|
file |
diff |
annotate
|
2010-12-17 |
haftmann |
avoid slightly odd Conv.tap_thy
|
file |
diff |
annotate
|
2010-12-17 |
wenzelm |
refer to regular structure Simplifier;
|
file |
diff |
annotate
|
2010-12-16 |
haftmann |
more uniform naming
|
file |
diff |
annotate
|
2010-12-15 |
haftmann |
simplified evaluation function names
|
file |
diff |
annotate
|
2010-09-21 |
haftmann |
no_frees_* is subsumed by new framework mechanisms in Code_Preproc
|
file |
diff |
annotate
|
2010-09-21 |
haftmann |
more conventional conversion signature
|
file |
diff |
annotate
|
2010-09-17 |
haftmann |
refined static_eval_conv_simple; tuned comments
|
file |
diff |
annotate
|
2010-09-16 |
haftmann |
separation of static and dynamic thy context
|
file |
diff |
annotate
|
2010-08-26 |
wenzelm |
simplification/standardization of some theory data;
|
file |
diff |
annotate
|
2010-08-23 |
haftmann |
use Code_Thingol.static_eval_conv_simple
|
file |
diff |
annotate
|
2010-08-23 |
haftmann |
refined and unified naming convention for dynamic code evaluation techniques
|
file |
diff |
annotate
|
2010-07-16 |
haftmann |
tuned interpunctation
|
file |
diff |
annotate
|
2010-07-08 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
2010-06-18 |
haftmann |
code_simp: only succeed on real progress
|
file |
diff |
annotate
|
2010-06-18 |
haftmann |
conclude simplification with default simpset
|
file |
diff |
annotate
|
2010-06-17 |
haftmann |
more precise code
|
file |
diff |
annotate
|
2010-06-17 |
haftmann |
added simp evaluator
|
file |
diff |
annotate
|
2010-06-15 |
haftmann |
added code_simp infrastructure
|
file |
diff |
annotate
|