Nominal-General/Nominal2_Eqvt.thy
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