author | haftmann |
Thu, 10 Sep 2009 15:23:07 +0200 | |
changeset 32554 | 4ccd84fb19d3 |
parent 32479 | 521cc9bf2958 |
child 34205 | f69cd974bc4e |
permissions | -rw-r--r-- |
(* Title: HOL/Extraction/ROOT.ML Examples for program extraction in Higher-Order Logic. *) if HOL_proofs < 2 then warning "HOL proof terms required for running extraction examples" else (Proofterm.proofs := 2; no_document use_thys ["Efficient_Nat", "~~/src/HOL/Old_Number_Theory/Factorization"]; use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"]);