src/HOLCF/Sprod2.ML
1995-02-07 clasohm 1995-02-07 added qed, qed_goal[w]
1994-01-19 nipkow 1994-01-19 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.