| Mon, 14 Apr 2025 20:19:05 +0200 |
haftmann |
revamped generation of functions
|
file |
diff |
annotate
|
| Sun, 06 Apr 2025 18:12:53 +0200 |
haftmann |
clarified variable names
|
file |
diff |
annotate
|
| Sun, 06 Apr 2025 18:12:52 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| 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
|
| 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
|