equal
deleted
inserted
replaced
56 |
56 |
57 fun mk_CollectC trm = |
57 fun mk_CollectC trm = |
58 let val T as Type ("fun",[t,_]) = fastype_of trm |
58 let val T as Type ("fun",[t,_]) = fastype_of trm |
59 in Collect_const t $ trm end; |
59 in Collect_const t $ trm end; |
60 |
60 |
61 fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT); |
61 fun inclt ty = Const (@{const_name Algebras.less_eq}, [ty,ty] ---> boolT); |
62 |
62 |
63 |
63 |
64 fun Mset ctxt prop = |
64 fun Mset ctxt prop = |
65 let |
65 let |
66 val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())]; |
66 val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())]; |