(* quick_and_dirty := true; *)
no_document use_thys ["~~/src/HOL/Library/LaTeXsugar",
                      "Name_Exec", "Lambda_Exec"];
use_thys ["Paper"];