add function mk_adm
authorhuffman
Fri Oct 15 06:08:42 2010 -0700 (2010-10-15)
changeset 40021d888417f7deb
parent 40020 0cbb08bf18df
child 40022 3a4a24b714f3
add function mk_adm
src/HOLCF/Tools/holcf_library.ML
     1.1 --- a/src/HOLCF/Tools/holcf_library.ML	Fri Oct 15 05:50:27 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/holcf_library.ML	Fri Oct 15 06:08:42 2010 -0700
     1.3 @@ -39,6 +39,9 @@
     1.4  
     1.5  fun mk_defined t = mk_not (mk_undef t);
     1.6  
     1.7 +fun mk_adm t =
     1.8 +  Const (@{const_name adm}, fastype_of t --> boolT) $ t;
     1.9 +
    1.10  fun mk_compact t =
    1.11    Const (@{const_name compact}, fastype_of t --> boolT) $ t;
    1.12