[1/3] 我太聪明了，在 ConTeXt 幻灯片里实现了自动输出 HOL4 定理排版。因为这件事已经比直接用 LaTeX 还要方便了，所以 LaTeX Beamer 我以后再也不用了）。