Various changes to support Nominal2 commands in local contexts.
quick_and_dirty := true;
no_document use_thys
["Lambda",
"Minimal",
"Tutorial1s",
"Tutorial3s",
"Tutorial4s",
"Tutorial1",
"Tutorial2",
"Tutorial2s",
"Tutorial3",
"Tutorial4",
"Tutorial5",
"Tutorial6"
];