Eliminated the prediates flat,chfin
Changed theorems with flat(x::'a) to (x::'a::flat)
Since flat<chfin theorems adm_flat,adm_flatdom are eliminated.
Use adm_chain_finite and adm_chfindom instead!
Examples do not use flat_flat any more
(* Title: HOLCF/Fun3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class instance of => (fun) for class pcpo
*)
Fun3 = Fun2 +
(* default class is still term *)
instance fun :: (term,cpo)cpo (cpo_fun)
instance fun :: (term,pcpo)pcpo (least_fun)
end