Nominal-General/Nominal2_Eqvt.thy
changeset 2303 c785fff02a8f
parent 2200 31f1ec832d39
child 2310 dd3b9c046c7d
equal deleted inserted replaced
2302:c6db12ddb60c 2303:c785fff02a8f
   381 apply(perm_simp)
   381 apply(perm_simp)
   382 oops
   382 oops
   383 
   383 
   384 declare [[trace_eqvt = false]]
   384 declare [[trace_eqvt = false]]
   385 
   385 
   386 text {* Problem: there is no raw eqvt-rule for The *}
   386 text {* there is no raw eqvt-rule for The *}
   387 lemma "p \<bullet> (THE x. P x) = foo"
   387 lemma "p \<bullet> (THE x. P x) = foo"
   388 apply(perm_strict_simp exclude: The)
   388 apply(perm_strict_simp exclude: The)
   389 apply(perm_simp exclude: The)
   389 apply(perm_simp exclude: The)
   390 oops
   390 oops
   391 
   391