src/HOLCF/lift1.thy
1994-01-26 nipkow 1994-01-26 case was renamed to sum_case
1994-01-19 nipkow 1994-01-19 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.