next up previous contents
Next: Library files for elimination Up: The LEGO library Previous: Natural Numbers: Basic theorems

Library files for eliminating over Type

 

The library directory lib_Type contains variants of all modules where SET, TYPE, TYPE_minus1 and TYPE_minus2 have been replaced by Type. This is a temporary patch to support true typical ambiguity.



Lego
Fri May 24 19:01:27 BST 1996