author  berghofe 
Fri, 16 Jul 1999 14:03:33 +0200  
changeset 7019  71f2155cdd85 
parent 6349  f7750d816c21 
child 8917  2ff6f8693c4f 
permissions  rwrr 
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"; 