ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
they can be proved trivially using eq_cs
ZF/domrange/XXX_empty: renamed XXX_0
(* Title: HOLCF/holcfb.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Basic definitions for the embedding of LCF into HOL.
*)
Holcfb = Nat +
consts
theleast :: "(nat=>bool)=>nat"
rules
theleast_def "theleast(P) == (@z.(P(z) & (!n.P(n)-->z<=n)))"
end