author | wenzelm |
Wed, 26 Jul 2006 00:44:44 +0200 | |
changeset 20207 | 4c57e850e8d5 |
parent 16417 | 9bc16273c2d4 |
child 22814 | 4cd25f1706bb |
permissions | -rw-r--r-- |
(* Title: ZF/Datatype.thy ID: $Id$ 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