Defining a non-concrete recursive type in HOL which includes sets
Files
Publication date
2000-02-18
Authors
Vos, T.E.J.
Swierstra, D.
Editors
Advisors
Supervisors
DOI
Document Type
Preprint
Metadata
Show full item recordCollections
License
Abstract
In HOL [GM93], a set of tools is provided which { for a certain class of commonly used
concrete recursive types { automatically carries out all the formal proofs necessary to define
these types.