| Mon, 15 May 2023 12:14:47 +0200 |
wenzelm |
proper trim_context / transfer;
|
changeset |
files
|
| Mon, 15 May 2023 10:59:49 +0200 |
wenzelm |
tuned: more accurate check (is_norm_hhf protect);
|
changeset |
files
|
| Mon, 15 May 2023 10:50:48 +0200 |
wenzelm |
clarified build options: reduce heap size by approx. 3%;
|
changeset |
files
|
| Sun, 14 May 2023 20:54:08 +0200 |
wenzelm |
more standard merge order, following logical structure of imports rather than physical serials;
|
changeset |
files
|
| Sun, 14 May 2023 13:15:52 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 14 May 2023 13:15:21 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 14 May 2023 13:00:49 +0200 |
wenzelm |
proper Thm.trim_context / Thm.transfer;
|
changeset |
files
|
| Sun, 14 May 2023 12:34:49 +0200 |
wenzelm |
proper Thm.trim_context / Thm.transfer;
|
changeset |
files
|
| Sat, 13 May 2023 21:30:34 +0200 |
wenzelm |
tuned: avoid pointless Proof_Context.init_global of Context.proof_of;
|
changeset |
files
|
| Thu, 18 May 2023 11:44:42 +0100 |
paulson |
New material from the HOL Light metric space library, mostly about quasi components
|
changeset |
files
|
| Mon, 15 May 2023 17:12:18 +0100 |
paulson |
More material from the HOL Light metric space library
|
changeset |
files
|
| Thu, 11 May 2023 22:12:43 +0200 |
wenzelm |
proper Thm.trim_context / Thm.transfer;
|
changeset |
files
|
| Thu, 11 May 2023 21:32:22 +0200 |
wenzelm |
proper position for ML-like commands;
|
changeset |
files
|
| Thu, 11 May 2023 14:17:24 +0200 |
wenzelm |
more robust: after shutdown;
|
changeset |
files
|