src/HOL/Proofs/Extraction/ROOT.ML

fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)

(* Examples for program extraction in Higher-Order Logic *)

no_document use_thys ["Efficient_Nat", "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"];