(* 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"];