equal
deleted
inserted
replaced
25 val mk_perm: term -> term -> term |
25 val mk_perm: term -> term -> term |
26 val dest_perm: term -> term * term |
26 val dest_perm: term -> term * term |
27 |
27 |
28 val mk_sort_of: term -> term |
28 val mk_sort_of: term -> term |
29 val atom_ty: typ -> typ |
29 val atom_ty: typ -> typ |
|
30 val atom_const: typ -> term |
30 val mk_atom_ty: typ -> term -> term |
31 val mk_atom_ty: typ -> term -> term |
31 val mk_atom: term -> term |
32 val mk_atom: term -> term |
32 |
33 |
33 val supp_ty: typ -> typ |
34 val supp_ty: typ -> typ |
34 val supp_const: typ -> term |
35 val supp_const: typ -> term |
126 | dest_perm t = raise TERM ("dest_perm", [t]); |
127 | dest_perm t = raise TERM ("dest_perm", [t]); |
127 |
128 |
128 fun mk_sort_of t = @{term "sort_of"} $ t; |
129 fun mk_sort_of t = @{term "sort_of"} $ t; |
129 |
130 |
130 fun atom_ty ty = ty --> @{typ "atom"}; |
131 fun atom_ty ty = ty --> @{typ "atom"}; |
131 fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t; |
132 fun atom_const ty = Const (@{const_name "atom"}, atom_ty ty) |
|
133 fun mk_atom_ty ty t = atom_const ty $ t; |
132 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
134 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
133 |
|
134 |
135 |
135 fun supp_ty ty = ty --> @{typ "atom set"}; |
136 fun supp_ty ty = ty --> @{typ "atom set"}; |
136 fun supp_const ty = Const (@{const_name supp}, supp_ty ty) |
137 fun supp_const ty = Const (@{const_name supp}, supp_ty ty) |
137 fun mk_supp_ty ty t = supp_const ty $ t |
138 fun mk_supp_ty ty t = supp_const ty $ t |
138 fun mk_supp t = mk_supp_ty (fastype_of t) t |
139 fun mk_supp t = mk_supp_ty (fastype_of t) t |