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 |
229 lemmas [eqvt] = |
231 lemmas [eqvt] = |
230 (* connectives *) |
232 (* connectives *) |
231 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
233 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
232 True_eqvt False_eqvt ex_eqvt all_eqvt |
234 True_eqvt False_eqvt ex_eqvt all_eqvt |
233 imp_eqvt [folded induct_implies_def] |
235 imp_eqvt [folded induct_implies_def] |
234 |
236 |
235 (* nominal *) |
237 (* nominal *) |
236 permute_eqvt supp_eqvt fresh_eqvt |
238 supp_eqvt fresh_eqvt permute_pure |
237 permute_pure |
|
238 |
239 |
239 (* datatypes *) |
240 (* datatypes *) |
240 permute_prod.simps |
241 permute_prod.simps |
241 fst_eqvt snd_eqvt |
242 fst_eqvt snd_eqvt |
242 |
243 |
243 (* sets *) |
244 (* sets *) |
244 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt |
245 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt |
245 Diff_eqvt Compl_eqvt insert_eqvt |
246 Diff_eqvt Compl_eqvt insert_eqvt |
|
247 |
|
248 lemmas [eqvt_raw] = permute_eqvt |
246 |
249 |
247 thm eqvts |
250 thm eqvts |
248 thm eqvts_raw |
251 thm eqvts_raw |
249 |
252 |
250 text {* helper lemmas for the eqvt_tac *} |
253 text {* helper lemmas for the eqvt_tac *} |