author | haftmann |
Wed, 03 Dec 2008 15:58:44 +0100 | |
changeset 28952 | 15a4b2cf8c34 |
parent 28229 | 4f06fae6a55e |
child 29125 | d41182a8135c |
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 |