replaced ML pokes by explicit usedir -p;
prefer -q 0 for proof terms, which avoids overhead of proof promises, while exploiting implicit parallelism of internal normalization;
(* Examples for program extraction in Higher-Order Logic *)
no_document use_thys ["Efficient_Nat", "~~/src/HOL/Number_Theory/UniqueFactorization"];
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];