author | oheimb |
Wed, 27 Oct 1999 19:32:19 +0200 | |
changeset 7958 | f531589c9fc1 |
parent 7019 | 71f2155cdd85 |
child 8917 | 2ff6f8693c4f |
permissions | -rw-r--r-- |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/Induct/ROOT |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
4 |
Copyright 1997 University of Cambridge |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
5 |
|
5078 | 6 |
Examples of Inductive and Coinductive Definitions |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
7 |
*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
8 |
|
6349
f7750d816c21
removed foo_build_completed -- now handled by session management (via usedir);
wenzelm
parents:
5739
diff
changeset
|
9 |
writeln"Root file for HOL/Induct"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
10 |
|
4449 | 11 |
set proof_timing; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
12 |
time_use_thy "Perm"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
13 |
time_use_thy "Comb"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
14 |
time_use_thy "Mutil"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
15 |
time_use_thy "Acc"; |
5628 | 16 |
time_use_thy "Multiset"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
17 |
time_use_thy "PropLog"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
18 |
time_use_thy "SList"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
19 |
time_use_thy "LFilter"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
20 |
time_use_thy "Term"; |
5739
f35761a1e1c4
Added new theory ABexp, removed obsolete theory Simult.
berghofe
parents:
5628
diff
changeset
|
21 |
time_use_thy "ABexp"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
22 |
time_use_thy "Exp"; |
7019 | 23 |
time_use_thy "Tree"; |