author | webertj |
Tue, 15 Jun 2004 00:06:40 +0200 | |
changeset 14942 | 78ddcbebace1 |
parent 13328 | 703de709a64b |
child 16417 | 9bc16273c2d4 |
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 = Inductive + Univ + QUniv files "Tools/datatype_package.ML" "Tools/numeral_syntax.ML": (*belongs to theory Bin*) end