add function mk_adm
authorhuffman
Fri, 15 Oct 2010 06:08:42 -0700
changeset 40021 d888417f7deb
parent 40020 0cbb08bf18df
child 40022 3a4a24b714f3
add function mk_adm
src/HOLCF/Tools/holcf_library.ML
--- 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;