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 [ |
3 no_document use_thys [ |
4 "~~/src/HOL/Library/Efficient_Nat", |
4 "~~/src/HOL/Library/Efficient_Nat", |
5 "~~/src/HOL/Library/Monad_Syntax", |
5 "~~/src/HOL/Library/Monad_Syntax", |
6 "~~/src/HOL/Number_Theory/Primes" |
6 "~~/src/HOL/Number_Theory/Primes", |
|
7 "~~/src/HOL/Number_Theory/UniqueFactorization", |
|
8 "~~/src/HOL/Library/State_Monad" |
7 ]; |
9 ]; |
8 |
10 |
9 share_common_data (); |
|
10 |
|
11 no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization", "~~/src/HOL/Library/State_Monad"]; |
|
12 use_thys ["Greatest_Common_Divisor", "Warshall", "Higman_Extraction", "Pigeonhole", "Euclid"]; |
11 use_thys ["Greatest_Common_Divisor", "Warshall", "Higman_Extraction", "Pigeonhole", "Euclid"]; |