| Mon, 04 Nov 2019 17:18:25 -0500 |
immler |
reduce dependencies of Ordered_Euclidean_Space; move more general material from Cartesian_Euclidean_Space
|
changeset |
files
|
| Mon, 04 Nov 2019 20:24:52 +0100 |
wenzelm |
proper message (amending 94442fce40a5);
|
changeset |
files
|
| Mon, 04 Nov 2019 20:10:23 +0100 |
wenzelm |
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;
|
changeset |
files
|
| Mon, 04 Nov 2019 16:56:16 +0100 |
wenzelm |
uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with export_proofs of re-used nodes;
|
changeset |
files
|
| Mon, 04 Nov 2019 15:15:56 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 04 Nov 2019 15:14:34 +0100 |
wenzelm |
updated xml_size;
|
changeset |
files
|
| Mon, 04 Nov 2019 15:06:54 +0100 |
wenzelm |
prefer named result;
|
changeset |
files
|
| Mon, 04 Nov 2019 14:56:49 +0100 |
wenzelm |
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
|
changeset |
files
|
| Sun, 03 Nov 2019 20:38:08 +0100 |
wenzelm |
expose derivations more thoroughly, notably for locale/class reasoning;
|
changeset |
files
|
| Sun, 03 Nov 2019 19:43:59 +0100 |
wenzelm |
clarified errors;
|
changeset |
files
|
| Sun, 03 Nov 2019 18:55:35 +0100 |
wenzelm |
determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
|
changeset |
files
|
| Sun, 03 Nov 2019 18:53:48 +0100 |
wenzelm |
more operations;
|
changeset |
files
|
| Sun, 03 Nov 2019 16:20:05 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sun, 03 Nov 2019 16:01:39 +0100 |
wenzelm |
more robust;
|
changeset |
files
|
| Sun, 03 Nov 2019 15:48:59 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|