equal
deleted
inserted
replaced
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 |