| author | wenzelm |
| Fri, 08 Apr 2011 22:50:50 +0200 | |
| changeset 42299 | 06e93f257d0e |
| parent 41413 | 64cd30d6b0b8 |
| child 45047 | 3aa8d3c391a4 |
| 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 |
|
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
39157
diff
changeset
|
3 |
no_document use_thys [ |
|
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
39157
diff
changeset
|
4 |
"~~/src/HOL/Library/Efficient_Nat", |
|
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
39157
diff
changeset
|
5 |
"~~/src/HOL/Library/Monad_Syntax", |
|
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
39157
diff
changeset
|
6 |
"~~/src/HOL/Number_Theory/Primes" |
|
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
39157
diff
changeset
|
7 |
]; |
|
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
39157
diff
changeset
|
8 |
|
|
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
|
9 |
share_common_data (); |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
39157
diff
changeset
|
10 |
|
|
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
|
11 |
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
|
12 |
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"]; |