| changeset 41429 | cf5f025bc3c7 |
| parent 40840 | 2f97215e79bf |
| child 42151 | 4da4fc77664b |
--- a/src/HOL/HOLCF/Tools/holcf_library.ML Mon Jan 03 17:10:32 2011 +0100 +++ b/src/HOL/HOLCF/Tools/holcf_library.ML Tue Jan 04 15:03:27 2011 -0800 @@ -32,7 +32,7 @@ (*** Basic HOLCF concepts ***) -fun mk_bottom T = Const (@{const_name UU}, T) +fun mk_bottom T = Const (@{const_name bottom}, T) fun below_const T = Const (@{const_name below}, [T, T] ---> boolT) fun mk_below (t, u) = below_const (fastype_of t) $ t $ u