Sat, 02 Dec 2023 15:42:50 +0100 | wenzelm | pro-forma support for optional zproof: no proper content yet; | file | diff | annotate |
Sat, 20 May 2023 17:42:01 +0200 | wenzelm | tuned signature; | file | diff | annotate |
Sat, 20 May 2023 16:12:37 +0200 | wenzelm | more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm); | file | diff | annotate |
Mon, 15 May 2023 14:09:45 +0200 | wenzelm | more operations "without_context", assuming that the thm has been properly transferred already; | file | diff | annotate |
Mon, 15 May 2023 10:59:49 +0200 | wenzelm | tuned: more accurate check (is_norm_hhf protect); | file | diff | annotate |
Tue, 18 Apr 2023 22:24:48 +0200 | wenzelm | tuned; | file | diff | annotate |
Mon, 05 Sep 2022 19:23:12 +0200 | wenzelm | tuned signature; | file | diff | annotate |