add functions mk_imp, mk_all
authorhuffman
Sat, 16 Oct 2010 14:41:11 -0700
changeset 40024 a0f760ef6995
parent 40023 a868e9d73031
child 40025 876689e6bbdf
add functions mk_imp, mk_all
src/HOLCF/Tools/holcf_library.ML
--- 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 ***)