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 |
|
72 |
67 |
73 (* fresh arguments for a term *) |
68 (* fresh arguments for a term *) |
74 val fresh_args: Proof.context -> term -> term list |
69 val fresh_args: Proof.context -> term -> term list |
75 |
70 |
76 (* datatype operations *) |
71 (* datatype operations *) |
211 fun to_set t = |
206 fun to_set t = |
212 if fastype_of t = @{typ "atom list"} |
207 if fastype_of t = @{typ "atom list"} |
213 then @{term "set :: atom list => atom set"} $ t |
208 then @{term "set :: atom list => atom set"} $ t |
214 else t |
209 else t |
215 |
210 |
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 |
211 |
223 |
212 |
224 |
213 |
225 (* produces fresh arguments for a term *) |
214 (* produces fresh arguments for a term *) |
226 |
215 |