| Sun, 06 Apr 2025 14:20:41 +0200 |
haftmann |
reflect nested lists in variables names
|
file |
diff |
annotate
|
| Fri, 04 Apr 2025 23:12:20 +0200 |
haftmann |
represent constants with explicit typargs to avoid false positives for equality approximations like ‹card UNIV === card UNIV›
|
file |
diff |
annotate
|
| Fri, 04 Apr 2025 23:12:19 +0200 |
haftmann |
restored type reconstruction for nbe: remaining type variables must remain schematic for checking
|
file |
diff |
annotate
|
| Fri, 04 Apr 2025 23:12:18 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 28 Mar 2025 14:13:38 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 28 Mar 2025 14:13:37 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 28 Mar 2025 14:13:36 +0100 |
haftmann |
spelling
|
file |
diff |
annotate
|
| Sat, 30 Nov 2024 16:01:58 +0100 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2024 17:40:15 +0100 |
wenzelm |
clarified signature: shorten common cases;
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 14:28:13 +0200 |
wenzelm |
clarified signature: more explicit operations;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2023 15:13:52 +0200 |
wenzelm |
clarified signature: more concise variations on implicit theory setup;
|
file |
diff |
annotate
|
| Fri, 24 Mar 2023 18:30:17 +0000 |
haftmann |
More explicit type information in dictionary arguments.
|
file |
diff |
annotate
|
| Thu, 09 Feb 2023 13:50:09 +0100 |
stuebinm |
explicit range types in abstractions
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Sat, 11 Sep 2021 22:07:43 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| 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
|