| changeset 40021 | d888417f7deb |
| parent 37108 | 00f13d3ad474 |
| child 40024 | a0f760ef6995 |
--- 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;