author | huffman |
Sat, 16 Oct 2010 14:41:11 -0700 | |
changeset 40024 | a0f760ef6995 |
parent 40023 | a868e9d73031 |
child 40025 | 876689e6bbdf |
--- a/src/HOLCF/Tools/holcf_library.ML Fri Oct 15 08:52:53 2010 -0700 +++ b/src/HOLCF/Tools/holcf_library.ML Sat Oct 16 14:41:11 2010 -0700 @@ -24,8 +24,10 @@ val mk_not = HOLogic.mk_not; val mk_conj = HOLogic.mk_conj; val mk_disj = HOLogic.mk_disj; +val mk_imp = HOLogic.mk_imp; fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t; +fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t; (*** Basic HOLCF concepts ***)