no_document 
use_thys ["../thys/turing_basic", 
          "../thys/turing_hoare",
          "../thys/uncomputable", 
          "../thys/abacus"(*,
          "../thys/rec_def",
          "../thys/recursive"*)];

use_thys ["Paper"]
