author | wenzelm |
Fri, 02 Oct 2009 23:15:36 +0200 | |
changeset 32863 | 5e8cef567042 |
parent 32479 | 521cc9bf2958 |
child 34205 | f69cd974bc4e |
permissions | -rw-r--r-- |
13405 | 1 |
(* Title: HOL/Extraction/ROOT.ML |
2 |
||
3 |
Examples for program extraction in Higher-Order Logic. |
|
4 |
*) |
|
5 |
||
6 |
if HOL_proofs < 2 then |
|
7 |
warning "HOL proof terms required for running extraction examples" |
|
8 |
else |
|
25374 | 9 |
(Proofterm.proofs := 2; |
32479 | 10 |
no_document use_thys ["Efficient_Nat", "~~/src/HOL/Old_Number_Theory/Factorization"]; |
25420
0fe95159787a
Added new exampes Greatest_Common_Divisor and Euclid.
berghofe
parents:
25374
diff
changeset
|
11 |
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"]); |