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

Re: [PVS-Help] loading files, indentation

R. Colvin writes:
   Date: Wed, 21 Apr 2004 10:08:29 +1000
   Subject: Re: [PVS-Help] loading files, indentation 
   
   John,
   
   On an unrelated topic, I have a sequent of the form:
   
   (exists (t: T): P1)
   |---------------
   	P2
   
Rewriting with "not_exists" gives you

   |---------------
   (forall (t: T): not P1)
   	P2

If you want to combine everything into one formula, then use
(skosimp) followed by (generalize "t!1" "t").


Bye,

Hendrik