src/HOL/Proofs/Extraction/ROOT.ML

shorten minimizer command further, exploiting until-now-undocumented syntax

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