| Wed, 31 Dec 2014 14:13:11 +0100 |
wenzelm |
more explict and generic field names
|
file |
diff |
annotate
|
| Wed, 31 Dec 2014 14:08:50 +0100 |
wenzelm |
uniform variable name for presentation graphs, to distinguish from values of type Graph.T
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 18:48:04 +0200 |
haftmann |
tuned data structure
|
file |
diff |
annotate
|
| Thu, 15 May 2014 16:38:31 +0200 |
haftmann |
syntactic means to prevent accidental mixup of static and dynamic context
|
file |
diff |
annotate
|
| Thu, 15 May 2014 16:38:29 +0200 |
haftmann |
dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
|
file |
diff |
annotate
|
| 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>;
|
file |
diff |
annotate
|
| Thu, 01 May 2014 09:30:35 +0200 |
haftmann |
optional case enforcement
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 11:42:32 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 14:37:14 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 11:57:52 +0100 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 16:30:01 +0100 |
haftmann |
dependency reporting for code generation errors
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 16:30:00 +0100 |
haftmann |
more abstract dictionary construction
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 16:09:04 +0100 |
haftmann |
reduced prominence of "permissive code generation"
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 23:50:49 +0100 |
haftmann |
less clumsy namespace
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 23:50:49 +0100 |
haftmann |
prefer explicit code symbol type over ad-hoc name mangling
|
file |
diff |
annotate
|
| Mon, 06 Jan 2014 09:31:19 +0100 |
haftmann |
special treatment of ==> and == solely as constants
|
file |
diff |
annotate
|
| Mon, 06 Jan 2014 09:31:18 +0100 |
haftmann |
uniform orientation of instances as (type constructor, type class)
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 01:05:46 +0100 |
haftmann |
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 22:31:34 +0200 |
wenzelm |
proper PIDE markup for codegen arguments;
|
file |
diff |
annotate
|
| Thu, 04 Jul 2013 08:52:44 +0200 |
haftmann |
explicit hint for domain of class parameters in instance statements
|
file |
diff |
annotate
|
| Sun, 26 May 2013 21:05:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 24 May 2013 23:57:24 +0200 |
haftmann |
bookkeeping and input syntax for exact specification of names of symbols in generated code
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 15:30:19 +0200 |
wenzelm |
more standard module name Axclass (according to file name);
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 15:29:25 +0200 |
wenzelm |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
|
file |
diff |
annotate
|
| Thu, 27 Dec 2012 21:01:08 +0100 |
haftmann |
more explicit name
|
file |
diff |
annotate
|
| Tue, 25 Sep 2012 15:40:41 +0200 |
wenzelm |
separate module Graph_Display;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2012 07:11:49 +0200 |
haftmann |
clarified code translation code
|
file |
diff |
annotate
|
| Tue, 05 Jun 2012 07:05:56 +0200 |
haftmann |
prefer records with speaking labels over deeply nested tuples
|
file |
diff |
annotate
|
| Mon, 28 May 2012 13:38:07 +0200 |
haftmann |
dropped sort constraints on datatype specifications
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 10:16:51 +0200 |
haftmann |
dropped dead code;
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 09:58:54 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 21:47:26 +0200 |
haftmann |
tuned name
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 21:11:50 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 10:29:45 +0200 |
Andreas Lochbihler |
generalise case certificates to allow ignored parameters
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Sat, 25 Feb 2012 12:34:56 +0100 |
wenzelm |
discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 15:49:40 +0100 |
wenzelm |
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 18:32:43 +0100 |
haftmann |
dropped disfruitful `constant signatures`
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 09:11:18 +0200 |
bulwahn |
removing dependency of the generic code generator to old code generator functions thyname_of_type and thyname_of_const
|
file |
diff |
annotate
|
| Wed, 12 Oct 2011 16:21:07 +0200 |
wenzelm |
discontinued obsolete alias structure ProofContext;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 09:30:19 +0200 |
bulwahn |
syntactic improvements and tuning names in the code generator due to Florian's code review
|
file |
diff |
annotate
|
| Mon, 19 Sep 2011 16:18:23 +0200 |
bulwahn |
adding abstraction layer; more precise function names
|
file |
diff |
annotate
|
| Mon, 19 Sep 2011 16:18:21 +0200 |
bulwahn |
adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used
|
file |
diff |
annotate
|
| Mon, 19 Sep 2011 16:18:19 +0200 |
bulwahn |
determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations
|
file |
diff |
annotate
|
| Mon, 19 Sep 2011 16:18:19 +0200 |
bulwahn |
only annotating constants with sort constraints
|
file |
diff |
annotate
|
| Mon, 19 Sep 2011 16:18:18 +0200 |
bulwahn |
also adding type annotations for the dynamic invocation
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 14:43:50 +0200 |
bulwahn |
stating more explicitly our expectation that these two terms have the same term structure
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 12:33:09 +0200 |
bulwahn |
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
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:39 +0200 |
bulwahn |
removing previously used function locally_monomorphic in the code generator
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:38 +0200 |
bulwahn |
setting const_sorts to false in the type inference of the code generator
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:36 +0200 |
bulwahn |
removing previous crude approximation to add type annotations to disambiguate types
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:35 +0200 |
bulwahn |
adding minimalistic implementation for printing the type annotations
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:34 +0200 |
bulwahn |
adding call to disambiguation annotations
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:34 +0200 |
bulwahn |
adding type inference for disambiguation annotations in code equation
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:32 +0200 |
bulwahn |
adding the body type as well to the code generation for constants as it is required for type annotations of constants
|
file |
diff |
annotate
|