2015-04-27 wenzelm 2015-04-27 code equations as displayable content in code dependency graph
2015-04-27 wenzelm 2015-04-27 filtering of reflexive dependencies avoids problems with state-of-the-art graph browser; clarified
2015-04-16 wenzelm 2015-04-16 discontinued pointless warnings: commands are only defined inside a theory context;
2015-04-16 wenzelm 2015-04-16 let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-24 wenzelm 2015-03-24 clarified input source;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-02-15 haftmann 2015-02-15 tuned
2015-02-15 haftmann 2015-02-15 purge variables not mentioned in body from pattern
2015-02-14 haftmann 2015-02-14 only collapse patterns with disjunctive variable names
2015-02-14 haftmann 2015-02-14 clarified
2014-12-31 wenzelm 2014-12-31 clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names); tuned;
2014-12-31 wenzelm 2014-12-31 for graph display, prefer graph data structure over list with dependencies; pragmatic distinction between (historically evolved) "session" nodes and (more abstract) "content" nodes
2014-12-31 wenzelm 2014-12-31 more explict and generic field names
2014-12-31 wenzelm 2014-12-31 uniform variable name for presentation graphs, to distinguish from values of type Graph.T
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-09-18 haftmann 2014-09-18 tuned data structure
2014-05-15 haftmann 2014-05-15 syntactic means to prevent accidental mixup of static and dynamic context
2014-05-15 haftmann 2014-05-15 dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
2014-05-09 haftmann 2014-05-09 normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>; tuned naming; dropped dead parameters;
2014-05-01 haftmann 2014-05-01 optional case enforcement
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-12 wenzelm 2014-03-12 tuned signature;
2014-03-10 wenzelm 2014-03-10 abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-02-26 haftmann 2014-02-26 prefer proof context over background theory
2014-01-30 haftmann 2014-01-30 dependency reporting for code generation errors
2014-01-30 haftmann 2014-01-30 more abstract dictionary construction
2014-01-30 haftmann 2014-01-30 reduced prominence of "permissive code generation"
2014-01-25 haftmann 2014-01-25 less clumsy namespace
2014-01-25 haftmann 2014-01-25 prefer explicit code symbol type over ad-hoc name mangling
2014-01-06 haftmann 2014-01-06 special treatment of ==> and == solely as constants
2014-01-06 haftmann 2014-01-06 uniform orientation of instances as (type constructor, type class)
2014-01-01 haftmann 2014-01-01 explicit distinction between empty code equations and no code equations, including convenient declaration attributes
2013-07-30 wenzelm 2013-07-30 proper PIDE markup for codegen arguments;
2013-07-04 haftmann 2013-07-04 explicit hint for domain of class parameters in instance statements
2013-05-26 wenzelm 2013-05-26 tuned;
2013-05-24 haftmann 2013-05-24 bookkeeping and input syntax for exact specification of names of symbols in generated code
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2013-04-09 wenzelm 2013-04-09 discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;
2012-12-27 haftmann 2012-12-27 more explicit name
2012-09-25 wenzelm 2012-09-25 separate module Graph_Display; tuned signature;
2012-06-05 haftmann 2012-06-05 clarified code translation code
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