| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Sun, 31 May 2015 00:17:47 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:56:43 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 20:09:31 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 12:56:06 +0100 |
wenzelm |
proper exception for internal program failure, not user-error;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 18:48:04 +0200 |
haftmann |
tuned data structure
|
file |
diff |
annotate
|
| Sun, 29 Jun 2014 18:02:18 +0200 |
haftmann |
modernized diagnostic options
|
file |
diff |
annotate
|
| Thu, 05 Jun 2014 11:11:41 +0200 |
haftmann |
be more explicit: made sml/nj happy
|
file |
diff |
annotate
|
| Thu, 15 May 2014 16:38:32 +0200 |
haftmann |
accurate separation of static and dynamic context
|
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:31 +0200 |
haftmann |
proper separation 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:36 +0200 |
haftmann |
degeneralized value command into HOL
|
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
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 11:57:52 +0100 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
| Wed, 29 Jan 2014 20:11:38 +0100 |
haftmann |
made smlnj happy
|
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
|
| Sun, 19 Jan 2014 11:05:38 +0100 |
haftmann |
prefer indexes user for pattern matching to print concrete names for symbols, do not rely on printable unique identifiers
|
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
|
| Thu, 04 Jul 2013 08:52:44 +0200 |
haftmann |
explicit hint for domain of class parameters in instance statements
|
file |
diff |
annotate
|
| Fri, 28 Jun 2013 21:07:41 +0200 |
haftmann |
formally accept dictionary parameters for constants on left hand sides in equations
|
file |
diff |
annotate
|
| Fri, 28 Jun 2013 21:07:32 +0200 |
haftmann |
do not choke on type variables emerging during rewriting
|
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, 05 Jun 2012 07:05:56 +0200 |
haftmann |
prefer records with speaking labels over deeply nested tuples
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 19:18:11 +0200 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 09:45:49 +0200 |
haftmann |
corrected Nbe.static_value: ignore cached compilations;
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 09:31:36 +0200 |
haftmann |
tuned heading
|
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
|
| Wed, 07 Sep 2011 13:51:30 +0200 |
bulwahn |
changing const type to pass along if typing annotations are necessary for disambigous terms
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 23:35:30 +0200 |
wenzelm |
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:16:03 +0200 |
wenzelm |
proper @{binding} antiquotations (relevant for formal references);
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 15:38:49 +0200 |
wenzelm |
prefer new-style Name.invents;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 20:47:02 +0200 |
wenzelm |
split Type_Infer into early and late part, after Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 17:14:48 +0100 |
wenzelm |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 09:18:29 +0100 |
haftmann |
canonical handling of theory context argument
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 18:24:44 +0100 |
haftmann |
avoid slightly odd Conv.tap_thy
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 09:47:12 +0100 |
haftmann |
simplified evaluation function names
|
file |
diff |
annotate
|
| Mon, 13 Dec 2010 22:54:47 +0100 |
haftmann |
separated dictionary weakning into separate type
|
file |
diff |
annotate
|
| Thu, 09 Dec 2010 17:25:43 +0100 |
haftmann |
dictionary constants must permit explicit weakening of classes;
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 21:32:47 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 09:36:12 +0100 |
haftmann |
removed experimental equality checking of closures; acknowledge underapproximation of equality in function name
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 23:13:58 +0100 |
haftmann |
nbe decides equality of abstractions by extensionality
|
file |
diff |
annotate
|
| Tue, 16 Nov 2010 10:33:36 +0100 |
haftmann |
added forall2 predicate lifter
|
file |
diff |
annotate
|
| Thu, 04 Nov 2010 17:27:38 +0100 |
haftmann |
Code.check_const etc.: reject too specific types
|
file |
diff |
annotate
|
| Fri, 01 Oct 2010 17:06:49 +0200 |
haftmann |
moved ML_Context.value to Code_Runtime
|
file |
diff |
annotate
|
| Tue, 21 Sep 2010 15:46:06 +0200 |
haftmann |
no_frees_* is subsumed by new framework mechanisms in Code_Preproc
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 16:51:34 +0200 |
haftmann |
separation of static and dynamic thy context
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 08:18:34 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 15:11:40 +0200 |
haftmann |
static nbe conversion
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 13:44:11 +0200 |
haftmann |
dropped redundant normal_form command
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 12:11:11 +0200 |
haftmann |
more clear separation of static compilation and dynamic evaluation
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 11:30:32 +0200 |
haftmann |
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
|
file |
diff |
annotate
|