author  paulson 
Tue, 09 Jul 2002 23:05:26 +0200  
changeset 13328  703de709a64b 
parent 12183  c10cea75dd56 
child 16417  9bc16273c2d4 
permissions  rwrr 
12175  1 
(* Title: ZF/Datatype.thy 
2870
6d6fd10a9fdc
Now a nontrivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset

2 
ID: $Id$ 
6d6fd10a9fdc
Now a nontrivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
6d6fd10a9fdc
Now a nontrivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset

4 
Copyright 1997 University of Cambridge 
6d6fd10a9fdc
Now a nontrivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset

5 

6d6fd10a9fdc
Now a nontrivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset

6 
*) 
516  7 

13328  8 
header{*Datatype and CoDatatype Definitions*} 
9 

12175  10 
theory Datatype = Inductive + Univ + QUniv 
12183  11 
files 
12 
"Tools/datatype_package.ML" 

13 
"Tools/numeral_syntax.ML": (*belongs to theory Bin*) 

12175  14 

15 
end 