equal
deleted
inserted
replaced
224 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *} |
224 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *} |
225 |
225 |
226 use "nominal_thmdecls.ML" |
226 use "nominal_thmdecls.ML" |
227 setup "Nominal_ThmDecls.setup" |
227 setup "Nominal_ThmDecls.setup" |
228 |
228 |
229 |
|
230 |
|
231 lemmas [eqvt] = |
229 lemmas [eqvt] = |
232 (* connectives *) |
230 (* connectives *) |
233 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
231 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
234 True_eqvt False_eqvt ex_eqvt all_eqvt |
232 True_eqvt False_eqvt ex_eqvt all_eqvt |
235 imp_eqvt [folded induct_implies_def] |
233 imp_eqvt [folded induct_implies_def] |
236 |
234 |
237 (* nominal *) |
235 (* nominal *) |
238 supp_eqvt fresh_eqvt permute_pure |
236 permute_eqvt supp_eqvt fresh_eqvt |
|
237 permute_pure |
239 |
238 |
240 (* datatypes *) |
239 (* datatypes *) |
241 permute_prod.simps |
240 permute_prod.simps |
242 fst_eqvt snd_eqvt |
241 fst_eqvt snd_eqvt |
243 |
242 |
244 (* sets *) |
243 (* sets *) |
245 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt |
244 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt |
246 Diff_eqvt Compl_eqvt insert_eqvt |
245 Diff_eqvt Compl_eqvt insert_eqvt |
247 |
|
248 lemmas [eqvt_raw] = permute_eqvt |
|
249 |
246 |
250 thm eqvts |
247 thm eqvts |
251 thm eqvts_raw |
248 thm eqvts_raw |
252 |
249 |
253 text {* helper lemmas for the eqvt_tac *} |
250 text {* helper lemmas for the eqvt_tac *} |