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 |