author | haftmann |
Mon, 05 Jul 2010 16:46:23 +0200 | |
changeset 37719 | 271ecd4fb9f9 |
parent 37296 | 1fad5b94c0ae |
child 37848 | a33ecf47f0a0 |
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 |
|
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"]; |