author | nipkow |
Fri, 26 Jan 2001 15:50:52 +0100 | |
changeset 10984 | 8f49dcbec859 |
parent 6070 | 032babd0120b |
child 12175 | 5cf58a1799a7 |
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 = Inductive + Univ + QUniv