equal
deleted
inserted
replaced
237 |
237 |
238 section {* Equivariance automation *} |
238 section {* Equivariance automation *} |
239 |
239 |
240 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
240 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
241 |
241 |
242 ML {* Thm.declaration_attribute *} |
|
243 |
|
244 use "nominal_thmdecls.ML" |
242 use "nominal_thmdecls.ML" |
245 setup "Nominal_ThmDecls.setup" |
243 setup "Nominal_ThmDecls.setup" |
246 |
244 |
247 lemmas [eqvt] = |
245 lemmas [eqvt] = |
248 (* connectives *) |
246 (* connectives *) |