src/HOL/Proofs/Extraction/ROOT.ML

avoid slightly odd share_common_data -- Poly/ML 5.5.x should manage low-memory situations (cf. f55e77f623ab);

(* 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",
  "~~/src/HOL/Number_Theory/UniqueFactorization",
  "~~/src/HOL/Library/State_Monad"
];

use_thys ["Greatest_Common_Divisor", "Warshall", "Higman_Extraction", "Pigeonhole", "Euclid"];