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