Please use this identifier to cite or link to this item:
http://hdl.handle.net/1880/46514| Title: | DEALING WITH THE CHOICE OPERATOR IN HOL88 |
| Authors: | Graham, Brian |
| Keywords: | Computer Science |
| Issue Date: | 1-Apr-1990 |
| Abstract: | This paper discusses the choice operator @ in HOL88. It gives an intuitive interpretation, as well as the definition, and presents proof strategies for goals that contain this operator, broken down into cases based on the number of values which satisfy the predicate argument. A working knowledge of the HOL system is assumed. |
| URI: | http://hdl.handle.net/1880/46514 |
| Appears in Collections: | Technical Reports |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| 1990-382-06.pdf | 1.65 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.