Sat, 30 Nov 2024 13:41:38 +0100 | wenzelm | tuned: more direct use of Name.context operations; | file | diff | annotate |
Fri, 29 Nov 2024 11:26:17 +0100 | wenzelm | tuned: more standard Name.build_context, although that is a bit longer; | file | diff | annotate |
Fri, 29 Nov 2024 00:25:03 +0100 | wenzelm | clarified signature: more uniform; | file | diff | annotate |
Sun, 04 Aug 2024 16:56:28 +0200 | wenzelm | tuned signature: more operations; | file | diff | annotate |
Fri, 19 Jul 2024 16:58:52 +0200 | wenzelm | clarified thm_header command_pos vs. thm_pos; | file | diff | annotate |
Fri, 07 Jun 2024 23:53:31 +0200 | wenzelm | more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name; | file | diff | annotate |