author | wenzelm |
Thu, 16 Feb 2006 18:25:54 +0100 | |
changeset 19070 | 99001616e0e2 |
parent 17024 | ae4a8446df16 |
child 23854 | 688a8a7bcd4e |
permissions | -rw-r--r-- |
13405 | 1 |
(* Title: HOL/Extraction/ROOT.ML |
2 |
ID: $Id$ |
|
3 |
||
4 |
Examples for program extraction in Higher-Order Logic. |
|
5 |
*) |
|
6 |
||
7 |
if HOL_proofs < 2 then |
|
8 |
warning "HOL proof terms required for running extraction examples" |
|
9 |
else |
|
10 |
(proofs := 2; |
|
11 |
time_use_thy "QuotRem"; |
|
12 |
time_use_thy "Warshall"; |
|
17024 | 13 |
time_use_thy "Higman"; |
14 |
no_document time_use_thy "EfficientNat"; |
|
15 |
time_use_thy "Pigeonhole"); |