equal
deleted
inserted
replaced
63 |
63 |
64 (** Makes Collect with type **) |
64 (** Makes Collect with type **) |
65 fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm |
65 fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm |
66 in Collect_const t $ trm end; |
66 in Collect_const t $ trm end; |
67 |
67 |
68 fun inclt ty = Const ("Orderings.less_eq", [ty,ty] ---> boolT); |
68 fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT); |
69 |
69 |
70 (** Makes "Mset <= t" **) |
70 (** Makes "Mset <= t" **) |
71 fun Mset_incl t = let val MsetT = fastype_of t |
71 fun Mset_incl t = let val MsetT = fastype_of t |
72 in mk_Trueprop ((inclt MsetT) $ Free ("Mset", MsetT) $ t) end; |
72 in mk_Trueprop ((inclt MsetT) $ Free ("Mset", MsetT) $ t) end; |
73 |
73 |