| changeset 459 | 4532577b61e0 |
| parent 448 | 957f69b9b7df |
| child 517 | d8c376662bb4 |
| 458:242e81f4d461 | 459:4532577b61e0 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory CallML |
2 theory CallML |
3 imports "~~/src/HOL/Number_Theory/Primes" Efficient_Nat |
3 imports "~~/src/HOL/Number_Theory/Primes" |
4 "~~/src/HOL/Library/Efficient_Nat" |
|
4 begin |
5 begin |
5 (*>*) |
6 (*>*) |
6 |
7 |
7 section {* Calling ML Functions from within HOL \label{rec:callml} *} |
8 section {* Calling ML Functions from within HOL \label{rec:callml} *} |
8 |
9 |