| author | blanchet |
| Wed, 15 Dec 2010 18:10:32 +0100 | |
| changeset 41171 | 043f8dc3b51f |
| parent 39157 | b98909faaea8 |
| child 41413 | 64cd30d6b0b8 |
| permissions | -rw-r--r-- |
|
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 | 2 |
|
|
38447
f55e77f623ab
HOL-Proofs-Extraction: some workaround to make it work in low-memory situations (e.g. atbroy102 with as little as 1GB heap space);
wenzelm
parents:
37848
diff
changeset
|
3 |
no_document use_thys ["Efficient_Nat", "Monad_Syntax", "~~/src/HOL/Number_Theory/Primes"]; |
|
f55e77f623ab
HOL-Proofs-Extraction: some workaround to make it work in low-memory situations (e.g. atbroy102 with as little as 1GB heap space);
wenzelm
parents:
37848
diff
changeset
|
4 |
share_common_data (); |
|
f55e77f623ab
HOL-Proofs-Extraction: some workaround to make it work in low-memory situations (e.g. atbroy102 with as little as 1GB heap space);
wenzelm
parents:
37848
diff
changeset
|
5 |
no_document use_thys ["~~/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
|
6 |
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"]; |