1 quick_and_dirty := true;
2 no_document use_thys ["../Nominal/Test"];
3 use_thys ["Paper"];
2 use_thys ["Paper"];