2012-06-05 haftmann 2012-06-05 prefer records with speaking labels over deeply nested tuples
2012-05-28 haftmann 2012-05-28 dropped sort constraints on datatype specifications
2012-04-19 haftmann 2012-04-19 dropped dead code; tuned
2012-04-19 haftmann 2012-04-19 tuned
2012-04-18 haftmann 2012-04-18 tuned name
2012-04-18 haftmann 2012-04-18 tuned
2012-04-12 Andreas Lochbihler 2012-04-12 generalise case certificates to allow ignored parameters
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-02-25 wenzelm 2012-02-25 discontinued slightly odd Graph.del_nodes (inefficient due to full;
2012-02-23 wenzelm 2012-02-23 clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
2011-12-26 haftmann 2011-12-26 dropped disfruitful `constant signatures`
2011-10-19 bulwahn 2011-10-19 removing dependency of the generic code generator to old code generator functions thyname_of_type and thyname_of_const
2011-10-12 wenzelm 2011-10-12 discontinued obsolete alias structure ProofContext;
2011-09-20 bulwahn 2011-09-20 syntactic improvements and tuning names in the code generator due to Florian's code review
2011-09-19 bulwahn 2011-09-19 adding abstraction layer; more precise function names
2011-09-19 bulwahn 2011-09-19 adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used
2011-09-19 bulwahn 2011-09-19 determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations
2011-09-19 bulwahn 2011-09-19 only annotating constants with sort constraints
2011-09-19 bulwahn 2011-09-19 also adding type annotations for the dynamic invocation
2011-09-09 bulwahn 2011-09-09 stating more explicitly our expectation that these two terms have the same term structure
2011-09-09 bulwahn 2011-09-09 revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
2011-09-07 bulwahn 2011-09-07 removing previously used function locally_monomorphic in the code generator
2011-09-07 bulwahn 2011-09-07 setting const_sorts to false in the type inference of the code generator
2011-09-07 bulwahn 2011-09-07 removing previous crude approximation to add type annotations to disambiguate types
2011-09-07 bulwahn 2011-09-07 adding minimalistic implementation for printing the type annotations
2011-09-07 bulwahn 2011-09-07 adding call to disambiguation annotations
2011-09-07 bulwahn 2011-09-07 adding type inference for disambiguation annotations in code equation
2011-09-07 bulwahn 2011-09-07 adding the body type as well to the code generation for constants as it is required for type annotations of constants
2011-09-07 bulwahn 2011-09-07 changing const type to pass along if typing annotations are necessary for disambigous terms
2011-08-20 wenzelm 2011-08-20 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-05-30 bulwahn 2011-05-30 improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
2011-04-18 wenzelm 2011-04-18 simplified Sorts.class_error: plain Proof.context; tuned;
2011-04-18 wenzelm 2011-04-18 simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
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