1 (* quick_and_dirty := true; *)

     2 no_document use_thys ["~~/src/HOL/Library/LaTeXsugar",

     3                       "Name_Exec", "Lambda_Exec"];

     4 use_thys ["Paper"];