author  wenzelm 
Fri, 01 Dec 2000 19:41:45 +0100  
changeset 10566  7ed4f5a6c63f 
parent 10259  93ec82d535f2 
child 10876  e12892e4666a 
permissions  rwrr 
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 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

6 
time_use_thy "Perm"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

7 
time_use_thy "Comb"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

8 
time_use_thy "Mutil"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

9 
time_use_thy "PropLog"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

10 
time_use_thy "SList"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

11 
time_use_thy "LFilter"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 
time_use_thy "Term"; 
5739
f35761a1e1c4
Added new theory ABexp, removed obsolete theory Simult.
berghofe
parents:
5628
diff
changeset

13 
time_use_thy "ABexp"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 
time_use_thy "Exp"; 
7019  15 
time_use_thy "Tree"; 