equal
deleted
inserted
replaced
62 val fold_append: term list -> term |
62 val fold_append: term list -> term |
63 val mk_conj: term * term -> term |
63 val mk_conj: term * term -> term |
64 val fold_conj: term list -> term |
64 val fold_conj: term list -> term |
65 |
65 |
66 val to_set: term -> term |
66 val to_set: term -> term |
|
67 |
|
68 (* some attributes *) |
|
69 val eqvt_attr : Args.src |
|
70 val rsp_attr : Args.src |
|
71 val simp_attr : Args.src |
67 |
72 |
68 (* fresh arguments for a term *) |
73 (* fresh arguments for a term *) |
69 val fresh_args: Proof.context -> term -> term list |
74 val fresh_args: Proof.context -> term -> term list |
70 |
75 |
71 (* datatype operations *) |
76 (* datatype operations *) |
207 if fastype_of t = @{typ "atom list"} |
212 if fastype_of t = @{typ "atom list"} |
208 then @{term "set :: atom list => atom set"} $ t |
213 then @{term "set :: atom list => atom set"} $ t |
209 else t |
214 else t |
210 |
215 |
211 |
216 |
|
217 (* some frequently used attributes *) |
|
218 |
|
219 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
|
220 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
|
221 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
|
222 |
|
223 |
|
224 |
212 (* produces fresh arguments for a term *) |
225 (* produces fresh arguments for a term *) |
213 |
226 |
214 fun fresh_args ctxt f = |
227 fun fresh_args ctxt f = |
215 f |> fastype_of |
228 f |> fastype_of |
216 |> binder_types |
229 |> binder_types |
222 |
235 |
223 (** datatypes **) |
236 (** datatypes **) |
224 |
237 |
225 (* constructor infos *) |
238 (* constructor infos *) |
226 type cns_info = (term * typ * typ list * bool list) list |
239 type cns_info = (term * typ * typ list * bool list) list |
|
240 |
|
241 (* - term for constructor constant |
|
242 - type of the constructor |
|
243 - types of the arguments |
|
244 - flags indicating whether the argument is recursive |
|
245 *) |
227 |
246 |
228 (* returns the type of the nth datatype *) |
247 (* returns the type of the nth datatype *) |
229 fun all_dtyps descr sorts = |
248 fun all_dtyps descr sorts = |
230 map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1)) |
249 map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1)) |
231 |
250 |