changeset 1866 | 6d4e4bf9bce6 |
parent 1835 | 636de31888a6 |
child 1867 | f4477d3fe520 |
--- a/Nominal-General/Nominal2_Eqvt.thy Fri Apr 16 11:09:32 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Fri Apr 16 16:29:11 2010 +0200 @@ -369,6 +369,7 @@ text {* Problem: there is no raw eqvt-rule for The *} lemma "p \<bullet> (THE x. P x) = foo" +apply(tactic {* Nominal_Permeq.eqvt_tac @{context} [] [@{const_name "The"}] 1*}) apply(perm_simp) (* apply(perm_strict_simp) *) oops