| changeset 31407 | 689df1591793 |
| parent 31406 | e23dd3aac0fb |
| parent 31385 | bc1f918ccf68 |
| child 31408 | 9f2ca03ae7b7 |
| 31406:e23dd3aac0fb | 31407:689df1591793 |
|---|---|
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 |