refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
(* Examples for program extraction in Higher-Order Logic *)
no_document use_thys [
"~~/src/HOL/Library/Efficient_Nat",
"~~/src/HOL/Library/Monad_Syntax",
"~~/src/HOL/Number_Theory/Primes"
];
share_common_data ();
no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"];
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];