src/HOLCF/Cfun1.ML
1995-02-07 clasohm 1995-02-07 added qed, qed_goal[w]
1994-11-28 regensbu 1994-11-28 ---------------------------------------------------------------------- Committing in HOLCF Use new translation mechanism and keyword syntax, cinfix.ML no longer needed. Optimized proofs in Cont.ML Modified Files: Cfun1.ML Cfun2.thy Cont.ML Cprod3.thy Makefile README Sprod3.thy Tr2.thy ccc1.thy ----------------------------------------------------------------------
1994-01-19 nipkow 1994-01-19 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.