| Tue, 28 Jan 2025 14:53:08 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 28 Jan 2025 13:42:40 +0100 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Tue, 28 Jan 2025 13:37:02 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 28 Jan 2025 13:35:08 +0100 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Tue, 28 Jan 2025 13:33:07 +0100 |
wenzelm |
minor performance tuning: avoid somewhat indirect filter / add_consts;
|
file |
diff |
annotate
|
| Tue, 28 Jan 2025 11:29:42 +0100 |
wenzelm |
clarified signature: more standard map_data;
|
file |
diff |
annotate
|
| Tue, 28 Jan 2025 11:20:53 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Tue, 28 Jan 2025 11:17:07 +0100 |
wenzelm |
clarified signature with minor performance tuning: avoid Context.proof_of with its Proof_Context.init_global;
|
file |
diff |
annotate
|
| Tue, 28 Jan 2025 11:05:45 +0100 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Mon, 27 Jan 2025 20:29:02 +0100 |
wenzelm |
support for "no" polarity of 'adhoc_overloading' vs. 'no_adhoc_overloading';
|
file |
diff |
annotate
|
| Mon, 27 Jan 2025 14:14:30 +0100 |
wenzelm |
clarified signature: proper ML interface to main command, without exposing too many internals;
|
file |
diff |
annotate
|
| Mon, 27 Jan 2025 12:52:19 +0100 |
wenzelm |
tuned signature: more explicit Type.raw_equiv;
|
file |
diff |
annotate
|
| Mon, 27 Jan 2025 12:24:51 +0100 |
wenzelm |
more liberal type equivalence, following thys/Transport/HOL_Basics/Adhoc_Overloading/Adhoc_Overloading.thy from AFP/e69d71bc07c4;
|
file |
diff |
annotate
|
| Mon, 27 Jan 2025 12:13:37 +0100 |
wenzelm |
move theory "HOL-Library.Adhoc_Overloading" to Pure;
|
file |
diff |
annotate
| base
|