author | huffman |
Fri, 15 Oct 2010 06:08:42 -0700 | |
changeset 40021 | d888417f7deb |
parent 40020 | 0cbb08bf18df |
child 40022 | 3a4a24b714f3 |
--- a/src/HOLCF/Tools/holcf_library.ML Fri Oct 15 05:50:27 2010 -0700 +++ b/src/HOLCF/Tools/holcf_library.ML Fri Oct 15 06:08:42 2010 -0700 @@ -39,6 +39,9 @@ fun mk_defined t = mk_not (mk_undef t); +fun mk_adm t = + Const (@{const_name adm}, fastype_of t --> boolT) $ t; + fun mk_compact t = Const (@{const_name compact}, fastype_of t --> boolT) $ t;