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