| author | wenzelm |
| Tue, 07 Apr 2009 23:25:50 +0200 | |
| changeset 30885 | a3cfe0e27deb |
| parent 30446 | e3641cac56fa |
| permissions | -rw-r--r-- |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28229
diff
changeset
|
1 |
(* Author: Florian Haftmann, TU Muenchen |
| 21917 | 2 |
*) |
3 |
||
4 |
header {* A huge set of executable constants *}
|
|
5 |
||
6 |
theory ExecutableContent |
|
7 |
imports |
|
| 27421 | 8 |
Complex_Main |
| 21917 | 9 |
AssocList |
10 |
Binomial |
|
11 |
Commutative_Ring |
|
| 27421 | 12 |
Enum |
| 21917 | 13 |
List_Prefix |
14 |
Nat_Infinity |
|
|
24433
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
24423
diff
changeset
|
15 |
Nested_Environment |
| 26515 | 16 |
Option_ord |
| 21917 | 17 |
Permutation |
18 |
Primes |
|
19 |
Product_ord |
|
20 |
SetsAndFunctions |
|
21 |
While_Combinator |
|
22 |
Word |
|
| 27421 | 23 |
"~~/src/HOL/ex/Commutative_Ring_Complete" |
24 |
"~~/src/HOL/ex/Records" |
|
| 21917 | 25 |
begin |
26 |
||
27 |
end |