| changeset 31382 | 5c563b968832 |
| parent 31374 | 8c8d615f04ae |
| parent 31381 | b3a785a69538 |
| child 31383 | ac7abb2e5944 |
| 31374:8c8d615f04ae | 31382:5c563b968832 |
|---|---|
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 |