| author | obua |
| Thu, 16 Feb 2006 14:59:57 +0100 | |
| changeset 19068 | 04b302f2902d |
| 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