src/Tools/Code/code_thingol.ML
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-02-17 haftmann 2011-02-17 added is_IAbs; tuned brackets and comments
2010-12-21 haftmann 2010-12-21 proper static closures
2010-12-21 haftmann 2010-12-21 canonical handling of theory context argument
2010-12-15 haftmann 2010-12-15 simplified evaluation function names
2010-12-13 haftmann 2010-12-13 separated dictionary weakning into separate type
2010-12-09 haftmann 2010-12-09 dictionary constants must permit explicit weakening of classes; tuned names
2010-12-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-11-26 haftmann 2010-11-26 keep type variable arguments of datatype constructors in bookkeeping
2010-11-26 haftmann 2010-11-26 globbing constant expressions use more idiomatic underscore rather than star
2010-09-20 haftmann 2010-09-20 Pure equality is a regular cpde operation
2010-09-17 haftmann 2010-09-17 proper closures for static evaluation; no need for FIXMEs any longer
2010-09-16 haftmann 2010-09-16 separation of static and dynamic thy context
2010-09-15 haftmann 2010-09-15 ignore code cache optionally
2010-09-07 haftmann 2010-09-07 dropped outdated substitution
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-23 haftmann 2010-08-23 preliminary versions of static_eval_conv(_simple)
2010-08-23 haftmann 2010-08-23 refined and unified naming convention for dynamic code evaluation techniques
2010-07-21 wenzelm 2010-07-21 replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
2010-07-16 haftmann 2010-07-16 don't fail gracefully
2010-07-08 haftmann 2010-07-08 tuned titles
2010-07-05 haftmann 2010-07-05 dropped passed irregular names
2010-07-02 haftmann 2010-07-02 reverted to verion from fc27be4c6b1c
2010-07-02 haftmann 2010-07-02 traceback for error messages
2010-06-30 haftmann 2010-06-30 unfold_fun_n
2010-06-17 haftmann 2010-06-17 explicit type variable arguments for constructors
2010-06-17 haftmann 2010-06-17 transitive superclasses were also only a misunderstanding
2010-06-17 haftmann 2010-06-17 formal introduction of transitive superclasses
2010-06-17 haftmann 2010-06-17 dropped obscure type argument weakening mapping -- was only a misunderstanding
2010-06-15 haftmann 2010-06-15 maintain cong rules for case combinators; more precise permissiveness
2010-06-15 haftmann 2010-06-15 formal introduction of case cong
2010-06-14 haftmann 2010-06-14 teaked naming of superclass projections
2010-06-07 haftmann 2010-06-07 more consistent naming aroud type classes and instances
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-04-21 haftmann 2010-04-21 optionally ignore errors during translation of equations; tuned representation of abstraction points
2010-04-19 haftmann 2010-04-19 more appropriate representation of valid positions for abstractors
2010-04-11 wenzelm 2010-04-11 of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
2010-03-25 wenzelm 2010-03-25 Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS); officially export weaken as Sorts.classrel_derivation; tuned comments;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-22 haftmann 2010-02-22 proper distinction of code datatypes and abstypes
2010-02-19 haftmann 2010-02-19 a simple concept for datatype invariants
2010-01-13 haftmann 2010-01-13 explicit abstract type of code certificates
2010-01-12 haftmann 2010-01-12 code certificates as integral part of code generation
2010-01-04 haftmann 2010-01-04 code cache only persists on equal theories
2010-01-04 haftmann 2010-01-04 code cache without copy; tuned
2009-12-23 haftmann 2009-12-23 reduced code generator cache to the baremost minimum
2009-12-14 haftmann 2009-12-14 explicit name for function space
2009-12-07 haftmann 2009-12-07 repaired read_const_expr, broken in 1e7ca47c6c3d
2009-12-04 haftmann 2009-12-04 merged, resolving minor conflicts
2009-12-04 haftmann 2009-12-04 avoid misleading name "superarities"
2009-12-04 haftmann 2009-12-04 merged
2009-11-30 haftmann 2009-11-30 dropped some unused bindings
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-12-02 haftmann 2009-12-02 subst_signatures
2009-11-03 haftmann 2009-11-03 pretty name for ==>
2009-10-26 haftmann 2009-10-26 tuned
2009-10-25 wenzelm 2009-10-25 maintain theory name via name space, not tags; AxClass.thynames_of_arity: explicit theory name, not tags;