Sciweavers

TPHOL
1999
IEEE
14 years 3 months ago
Disjoint Sums over Type Classes in HOL
The standard versions of HOL only support disjoint sums over finite families of types. This paper introduces disjoint sums over type classes containing possibly a countably infinit...
Norbert Völker