author | berghofe |
Mon, 19 Nov 2001 17:40:45 +0100 | |
changeset 12238 | 09966ccbc84c |
parent 12183 | c10cea75dd56 |
child 13328 | 703de709a64b |
permissions | -rw-r--r-- |
(* 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" "Tools/numeral_syntax.ML": (*belongs to theory Bin*) end