| author | wenzelm |
| Fri, 12 Jan 2001 11:08:06 +0100 | |
| changeset 10876 | e12892e4666a |
| parent 10566 | 7ed4f5a6c63f |
| child 11046 | b5f5942781a0 |
| permissions | -rw-r--r-- |
| 9450 | 1 |
(* Title: HOL/Induct/ROOT.ML |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
2 |
|
| 9450 | 3 |
Examples of Inductive and Coinductive Definitions. |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
4 |
*) |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
5 |
|
| 10876 | 6 |
time_use_thy "Sigma_Algebra"; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
7 |
time_use_thy "Perm"; |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
8 |
time_use_thy "Comb"; |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
9 |
time_use_thy "Mutil"; |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
10 |
time_use_thy "PropLog"; |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
11 |
time_use_thy "SList"; |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
12 |
time_use_thy "LFilter"; |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
13 |
time_use_thy "Term"; |
|
5739
f35761a1e1c4
Added new theory ABexp, removed obsolete theory Simult.
berghofe
parents:
5628
diff
changeset
|
14 |
time_use_thy "ABexp"; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
15 |
time_use_thy "Exp"; |
| 7019 | 16 |
time_use_thy "Tree"; |