add functions mk_imp, mk_all
authorhuffman
Sat Oct 16 14:41:11 2010 -0700 (2010-10-16)
changeset 40024a0f760ef6995
parent 40023 a868e9d73031
child 40025 876689e6bbdf
add functions mk_imp, mk_all
src/HOLCF/Tools/holcf_library.ML
     1.1 --- a/src/HOLCF/Tools/holcf_library.ML	Fri Oct 15 08:52:53 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/holcf_library.ML	Sat Oct 16 14:41:11 2010 -0700
     1.3 @@ -24,8 +24,10 @@
     1.4  val mk_not = HOLogic.mk_not;
     1.5  val mk_conj = HOLogic.mk_conj;
     1.6  val mk_disj = HOLogic.mk_disj;
     1.7 +val mk_imp = HOLogic.mk_imp;
     1.8  
     1.9  fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t;
    1.10 +fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t;
    1.11  
    1.12  
    1.13  (*** Basic HOLCF concepts ***)