| author | huffman |
| Tue, 02 Mar 2010 09:54:50 -0800 | |
| changeset 35512 | d1ef88d7de5a |
| parent 34205 | f69cd974bc4e |
| child 37288 | 2b1c6dd48995 |
| 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 |
|
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
32479
diff
changeset
|
3 |
Proofterm.proofs := 2; |
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
32479
diff
changeset
|
4 |
|
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
32479
diff
changeset
|
5 |
no_document use_thys ["Efficient_Nat", "~~/src/HOL/Old_Number_Theory/Factorization"]; |
|
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"]; |