author | berghofe |
Wed, 11 Jul 2007 11:14:51 +0200 | |
changeset 23746 | a455e69c31cc |
parent 17598 | 7540ccd2b445 |
child 24104 | 719fbe4fb77f |
permissions | -rw-r--r-- |
17598 | 1 |
|
2 |
(* $Id$ *) |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
3 |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
10876
diff
changeset
|
4 |
time_use_thy "Mutil"; |
14527 | 5 |
time_use_thy "QuoDataType"; |
15172 | 6 |
time_use_thy "QuoNestedDataType"; |
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
10876
diff
changeset
|
7 |
time_use_thy "Term"; |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
10876
diff
changeset
|
8 |
time_use_thy "ABexp"; |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
10876
diff
changeset
|
9 |
time_use_thy "Tree"; |
11641 | 10 |
time_use_thy "Ordinals"; |
10876 | 11 |
time_use_thy "Sigma_Algebra"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
12 |
time_use_thy "Comb"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
13 |
time_use_thy "PropLog"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
14 |
time_use_thy "SList"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
15 |
time_use_thy "LFilter"; |
23746 | 16 |
time_use_thy "Com"; |