Re: Judgements and TCCs for numerals

[Hanne Gottliebsen <hago@dcs.st-and.ac.uk>]

John,

> We are thinking of adding a facility to PVS 3.0 that will optionally
> check whether TCCs are evaluable and will suppress those that can be
> discharged by the PVS evaluator.  This will solve your problem but I'm
> afraid you'll have to wait for the new version of PVS.  Our goal is to
> release it in June.

Thanks for letting me know, and on that note I would like to encourage you
to add that facility :-)

Thanks,
Hanne
---------------------------------------------------------
Hanne Gottliebsen		    Office P337
Dept. of Computer Science	    Ph: +44 1334 46 3265
University of St Andrews	    hago@dcs.st-and.ac.uk
  - I want a single-skin cotton tent like Mr Weasley's
---------------------------------------------------------