| author | wenzelm |
| Sun, 20 May 2012 11:34:33 +0200 | |
| changeset 47884 | 21c42b095c84 |
| parent 45047 | 3aa8d3c391a4 |
| child 48274 | c8dce1689f79 |
| 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 |
|
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
41413
diff
changeset
|
11 |
no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization", "~~/src/HOL/Library/State_Monad"]; |
|
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
41413
diff
changeset
|
12 |
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman_Extraction", "Pigeonhole", "Euclid"]; |