equal
deleted
inserted
replaced
1 (* Examples for program extraction in Higher-Order Logic *) |
1 (* Examples for program extraction in Higher-Order Logic *) |
2 |
2 |
3 no_document use_thys ["Efficient_Nat", "Monad_Syntax", "~~/src/HOL/Number_Theory/Primes"]; |
3 no_document use_thys [ |
|
4 "~~/src/HOL/Library/Efficient_Nat", |
|
5 "~~/src/HOL/Library/Monad_Syntax", |
|
6 "~~/src/HOL/Number_Theory/Primes" |
|
7 ]; |
|
8 |
4 share_common_data (); |
9 share_common_data (); |
|
10 |
5 no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"]; |
11 no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"]; |
6 use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"]; |
12 use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"]; |