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

Re: Question on new decision procedures



Tamarah,

> Also, I did not manage to find the epsilon and choose functions in the 
> manuals. Did I just miss them (and then, please where are they) or are
> they not there and being phased out?

There's some discussion of epsilon and choose in section 2.4.2 of the
"less elementary" tutorial:
  http://pvs.csl.sri.com/pvs/examples/elementary-tutorial/csl-95-10.html

And also in the "Subtypes for Specifications" paper:
  http://www.csl.sri.com/reports/html/tse98.html

As Harald says, there's no danger of these being phased out.
John
-------