equal
deleted
inserted
replaced
367 |
367 |
368 declare [[trace_eqvt = false]] |
368 declare [[trace_eqvt = false]] |
369 |
369 |
370 text {* Problem: there is no raw eqvt-rule for The *} |
370 text {* Problem: there is no raw eqvt-rule for The *} |
371 lemma "p \<bullet> (THE x. P x) = foo" |
371 lemma "p \<bullet> (THE x. P x) = foo" |
|
372 apply(tactic {* Nominal_Permeq.eqvt_tac @{context} [] [@{const_name "The"}] 1*}) |
372 apply(perm_simp) |
373 apply(perm_simp) |
373 (* apply(perm_strict_simp) *) |
374 (* apply(perm_strict_simp) *) |
374 oops |
375 oops |
375 |
376 |
376 (* automatic equivariance procedure for |
377 (* automatic equivariance procedure for |