Wed, 12 May 2010 23:54:00 +0200 |
use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)
|
file | diff | annotate |