Up to index of Isabelle/ZF
theory Datatype(* Title: ZF/Datatype.thy ID: $Id: Datatype.thy,v 1.11 2005/06/17 14:15:09 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge *) header{*Datatype and CoDatatype Definitions*} theory Datatype imports Inductive Univ QUniv uses "Tools/datatype_package.ML" "Tools/numeral_syntax.ML" begin (*belongs to theory Bin*) end