src/HOL/Extraction/ROOT.ML
author wenzelm
Wed, 02 Jun 2010 21:12:28 +0200
changeset 37296 1fad5b94c0ae
parent 37288 2b1c6dd48995
child 37848 a33ecf47f0a0
permissions -rw-r--r--
replaced ML pokes by explicit usedir -p; prefer -q 0 for proof terms, which avoids overhead of proof promises, while exploiting implicit parallelism of internal normalization;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 32479
diff changeset
     1
(* Examples for program extraction in Higher-Order Logic *)
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
     2
37288
2b1c6dd48995 removed dependency of Euclid on Old_Number_Theory
haftmann
parents: 34205
diff changeset
     3
no_document use_thys ["Efficient_Nat", "~~/src/HOL/Number_Theory/UniqueFactorization"];
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 32479
diff changeset
     4
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];