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

[PVS-Help] Automatic simplification

To: pvs-help@xxxxxxxxxxx
Subject: [PVS-Help] Automatic simplification
From: Johannes Eriksson <joheriks@xxxxxx>
Date: Wed, 2 Sep 2009 18:42:08 +0300
List-Help: <mailto:pvs-help-request@csl.sri.com?subject=help>
List-Id: PVS-Help <pvs-help.csl.sri.com>
List-Post: <mailto:pvs-help@csl.sri.com>
List-Subscribe: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>
List-Unsubscribe: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>
Sender: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx
User-Agent: Mutt/1.5.18 (2008-05-17)

Hello,

A simple question: The PVS prover automatically applies (propax) to
every generated sequent; how does one disable this behavior?

Regards,
Johannes

-- 
Johannes W. E. Eriksson, M.Sc.
Ph.D. Student / Turku Centre For Computer Science (TUCS)
Åbo Akademi University / Department of Information Technologies
e-mail: joheriks@abo.fi  www: http://www.abo.fi/~joheriks

Prev by Date: [PVS-Help] (no subject)
Next by Date: Re: [PVS-Help] (no subject)
Prev by thread: [PVS-HELP] Function type extend problem
Next by thread: [PVS-Help] extend
Index(es):
- Date
- Thread