| Tue, 19 Dec 2023 23:06:26 +0100 | wenzelm | merged | changeset | files |
| Tue, 19 Dec 2023 22:56:32 +0100 | wenzelm | use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes; | changeset | files |
| Tue, 19 Dec 2023 20:02:17 +0100 | wenzelm | clarified signature; | changeset | files |
| Tue, 19 Dec 2023 19:20:21 +0100 | wenzelm | omit pointless future: proof terms are built sequentially; | changeset | files |
| Tue, 19 Dec 2023 19:18:09 +0100 | wenzelm | omit unclear / inaccurate renaming; | changeset | files |
| Tue, 19 Dec 2023 18:03:25 +0100 | wenzelm | more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm; | changeset | files |
| Tue, 19 Dec 2023 17:54:55 +0100 | wenzelm | more robust: avoid assumption about Context.certificate_theory; | changeset | files |
| Tue, 19 Dec 2023 17:31:12 +0100 | wenzelm | tuned; | changeset | files |