adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2)
(* Examples for program extraction in Higher-Order Logic *)
Proofterm.proofs := 2;
no_document use_thys ["Efficient_Nat", "~~/src/HOL/Old_Number_Theory/Factorization"];
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];