| Tue, 26 Dec 2023 12:46:10 +0100 | wenzelm | more robust: avoid crash of Thm.solve_constraints due to changed background theory, e.g. relevant for AFP/Transition_Systems_and_Automata; | changeset | files |
| Tue, 26 Dec 2023 12:37:33 +0100 | wenzelm | clarified signature; | changeset | files |
| Tue, 26 Dec 2023 12:03:54 +0100 | wenzelm | proper Thm_Name.make_list for thm_definition; | changeset | files |
| Sun, 24 Dec 2023 20:35:22 +0100 | wenzelm | more robust: avoid crash of AFP/Transition_Systems_and_Automata (amending fe4bd39bfeac and 43d8385db923); | changeset | files |
| Sun, 24 Dec 2023 20:17:08 +0100 | wenzelm | more robust: zproofs need to be enabled (amending 43d8385db923); | changeset | files |
| Sun, 24 Dec 2023 13:58:25 +0100 | wenzelm | more thorough thm definition via Global_Theory.register_proofs: store (and purge) zproofs; | changeset | files |
| Sun, 24 Dec 2023 13:20:40 +0100 | wenzelm | tuned names; | changeset | files |
| Sun, 24 Dec 2023 13:08:34 +0100 | wenzelm | clarified signature: support update of local_theory; | changeset | files |