Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
optional timing for code generator conversions
|
file |
diff |
annotate
|
Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
explicit quasi-global context for nbe conversions -- works around quasi-global type variable handling in lift_triv_classes_conv
|
file |
diff |
annotate
|
Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified naming conventions and code for code evaluation sandwiches
|
file |
diff |
annotate
|
Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified names of variants
|
file |
diff |
annotate
|
Tue, 12 Apr 2016 14:38:57 +0200 |
wenzelm |
Type_Infer.object_logic controls improvement of type inference result;
|
file |
diff |
annotate
|
Tue, 08 Mar 2016 21:07:48 +0100 |
haftmann |
explicit record values for dictionary variables
|
file |
diff |
annotate
|
Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
Wed, 02 Sep 2015 23:17:18 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
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
|