Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
uses lemma sum_bij; proof of prod_eqpoll_cong uses lemma prod_bij.
(* Title: HOLCF/HOLCF.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Top theory for HOLCF system
*)
HOLCF = Tr2