| author | wenzelm |
| Tue, 20 Oct 1998 16:26:20 +0200 | |
| changeset 5686 | 1f053d05f571 |
| parent 2870 | 6d6fd10a9fdc |
| child 6053 | 8a1059aa01f0 |
| permissions | -rw-r--r-- |
(* Title: ZF/Datatype ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge Dummy theory: brings in all ancestors needed for (Co)Datatype Declarations "Datatype" must be capital to avoid conflicts with ML's "datatype" *) Datatype = "constructor" + Inductive + Univ + QUniv + end