(* Title: ZF/Datatype.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory.*)theory Datatype = Inductive + Univ + QUniv files "Tools/datatype_package.ML":end