[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Looking for old finite_set library



Guru,

> I need the old pvs finite_set library.
> Specially I am interested in the following two LEMMA's
> finite_union: LEMMA is_finite(union(A,B))
> finite_intersection: LEMMA is_finite(intersection(A,B))

These lemmas and their proofs are in the prelude.  Finite_union is now
stated as a JUDGEMENT, so you have to do M-x vpf, search for the
formula, then do M-x tcc, then go to the corresponding OBLIGATION in
the tcc buffer and do M-x edit-proof.

John