src/Tools/Code/code_thingol.ML
Thu, 13 Apr 2017 10:10:12 +0200 haftmann for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness
Thu, 26 Jan 2017 16:06:19 +0100 haftmann tuned structure and terminology
Tue, 14 Jun 2016 20:48:41 +0200 haftmann explicit resolution of ambiguous dictionaries
Sun, 29 May 2016 14:43:18 +0200 haftmann explicit check that abstract constructors cannot be part of official interface
Thu, 26 May 2016 15:27:50 +0200 haftmann optional timing for code generator conversions
Thu, 26 May 2016 15:27:50 +0200 haftmann corrected closure scope of static_conv_thingol;
Thu, 26 May 2016 15:27:50 +0200 haftmann clarified proof context vs. background theory
Thu, 26 May 2016 15:27:50 +0200 haftmann clarified naming conventions and code for code evaluation sandwiches
Thu, 26 May 2016 15:27:50 +0200 haftmann clarified names of variants
Mon, 09 May 2016 14:37:47 +0200 wenzelm clarified context, notably for internal use of Simplifier;
Tue, 08 Mar 2016 21:07:48 +0100 haftmann explicit record values for dictionary variables
Tue, 08 Mar 2016 21:07:47 +0100 haftmann provide explicit hint concering uniqueness of derivation
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Fri, 25 Sep 2015 19:13:47 +0200 wenzelm tuned signature: eliminated pointless type Context.pretty;
Thu, 09 Jul 2015 00:39:49 +0200 wenzelm clarified context;
Mon, 27 Apr 2015 16:46:52 +0200 wenzelm code equations as displayable content in code dependency graph
Mon, 27 Apr 2015 15:53:11 +0200 wenzelm filtering of reflexive dependencies avoids problems with state-of-the-art graph browser;
Thu, 16 Apr 2015 15:22:44 +0200 wenzelm discontinued pointless warnings: commands are only defined inside a theory context;
Thu, 16 Apr 2015 11:22:36 +0200 wenzelm let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Tue, 24 Mar 2015 11:53:18 +0100 wenzelm clarified input source;
Fri, 06 Mar 2015 23:52:14 +0100 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Sun, 15 Feb 2015 08:17:46 +0100 haftmann tuned
Sun, 15 Feb 2015 08:17:44 +0100 haftmann purge variables not mentioned in body from pattern
Sat, 14 Feb 2015 19:57:26 +0100 haftmann only collapse patterns with disjunctive variable names
Sat, 14 Feb 2015 19:57:24 +0100 haftmann clarified
Wed, 31 Dec 2014 20:42:45 +0100 wenzelm clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
Wed, 31 Dec 2014 14:15:52 +0100 wenzelm for graph display, prefer graph data structure over list with dependencies;
Wed, 31 Dec 2014 14:13:11 +0100 wenzelm more explict and generic field names
Wed, 31 Dec 2014 14:08:50 +0100 wenzelm uniform variable name for presentation graphs, to distinguish from values of type Graph.T
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Mon, 03 Nov 2014 14:50:27 +0100 wenzelm eliminated unused int_only flag (see also c12484a27367);
Thu, 18 Sep 2014 18:48:04 +0200 haftmann tuned data structure
Thu, 15 May 2014 16:38:31 +0200 haftmann syntactic means to prevent accidental mixup of static and dynamic context
Thu, 15 May 2014 16:38:29 +0200 haftmann dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
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>;
Thu, 01 May 2014 09:30:35 +0200 haftmann optional case enforcement
Fri, 21 Mar 2014 11:42:32 +0100 wenzelm more qualified names;
Wed, 12 Mar 2014 14:37:14 +0100 wenzelm tuned signature;
Mon, 10 Mar 2014 13:55:03 +0100 wenzelm abstract type Name_Space.table;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Wed, 26 Feb 2014 11:57:52 +0100 haftmann prefer proof context over background theory
Thu, 30 Jan 2014 16:30:01 +0100 haftmann dependency reporting for code generation errors
Thu, 30 Jan 2014 16:30:00 +0100 haftmann more abstract dictionary construction
Thu, 30 Jan 2014 16:09:04 +0100 haftmann reduced prominence of "permissive code generation"
Sat, 25 Jan 2014 23:50:49 +0100 haftmann less clumsy namespace
Sat, 25 Jan 2014 23:50:49 +0100 haftmann prefer explicit code symbol type over ad-hoc name mangling
Mon, 06 Jan 2014 09:31:19 +0100 haftmann special treatment of ==> and == solely as constants
Mon, 06 Jan 2014 09:31:18 +0100 haftmann uniform orientation of instances as (type constructor, type class)
Wed, 01 Jan 2014 01:05:46 +0100 haftmann explicit distinction between empty code equations and no code equations, including convenient declaration attributes
Tue, 30 Jul 2013 22:31:34 +0200 wenzelm proper PIDE markup for codegen arguments;
Thu, 04 Jul 2013 08:52:44 +0200 haftmann explicit hint for domain of class parameters in instance statements
Sun, 26 May 2013 21:05:03 +0200 wenzelm tuned;
Fri, 24 May 2013 23:57:24 +0200 haftmann bookkeeping and input syntax for exact specification of names of symbols in generated code
Wed, 10 Apr 2013 15:30:19 +0200 wenzelm more standard module name Axclass (according to file name);
Tue, 09 Apr 2013 15:29:25 +0200 wenzelm discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
Thu, 27 Dec 2012 21:01:08 +0100 haftmann more explicit name
Tue, 25 Sep 2012 15:40:41 +0200 wenzelm separate module Graph_Display;
Tue, 05 Jun 2012 07:11:49 +0200 haftmann clarified code translation code
less more (0) -100 -60 tip