src/HOLCF/Tools/holcf_library.ML
changeset 40024 a0f760ef6995
parent 40021 d888417f7deb
child 40212 20df78048db5
equal deleted inserted replaced
40023:a868e9d73031 40024:a0f760ef6995
    22 val mk_fst = HOLogic.mk_fst;
    22 val mk_fst = HOLogic.mk_fst;
    23 val mk_snd = HOLogic.mk_snd;
    23 val mk_snd = HOLogic.mk_snd;
    24 val mk_not = HOLogic.mk_not;
    24 val mk_not = HOLogic.mk_not;
    25 val mk_conj = HOLogic.mk_conj;
    25 val mk_conj = HOLogic.mk_conj;
    26 val mk_disj = HOLogic.mk_disj;
    26 val mk_disj = HOLogic.mk_disj;
       
    27 val mk_imp = HOLogic.mk_imp;
    27 
    28 
    28 fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t;
    29 fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t;
       
    30 fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t;
    29 
    31 
    30 
    32 
    31 (*** Basic HOLCF concepts ***)
    33 (*** Basic HOLCF concepts ***)
    32 
    34 
    33 fun mk_bottom T = Const (@{const_name UU}, T);
    35 fun mk_bottom T = Const (@{const_name UU}, T);