| changeset 31378 | d1cbf6393964 |
| parent 31377 | a48f9ef9de15 |
| child 31379 | 213299656575 |
| 31377:a48f9ef9de15 | 31378:d1cbf6393964 |
|---|---|
1 (* Author: Florian Haftmann, TU Muenchen |
|
2 *) |
|
3 |
|
4 header {* A huge set of executable constants *} |
|
5 |
|
6 theory ExecutableContent |
|
7 imports |
|
8 Complex_Main |
|
9 AssocList |
|
10 Binomial |
|
11 Commutative_Ring |
|
12 Enum |
|
13 List_Prefix |
|
14 Nat_Infinity |
|
15 Nested_Environment |
|
16 Option_ord |
|
17 Permutation |
|
18 Primes |
|
19 Product_ord |
|
20 SetsAndFunctions |
|
21 While_Combinator |
|
22 Word |
|
23 "~~/src/HOL/ex/Commutative_Ring_Complete" |
|
24 "~~/src/HOL/ex/Records" |
|
25 begin |
|
26 |
|
27 end |