equal
deleted
inserted
replaced
382 lemma "p \<bullet> (THE x. P x) = foo" |
382 lemma "p \<bullet> (THE x. P x) = foo" |
383 apply(perm_strict_simp exclude: The) |
383 apply(perm_strict_simp exclude: The) |
384 apply(perm_simp exclude: The) |
384 apply(perm_simp exclude: The) |
385 oops |
385 oops |
386 |
386 |
|
387 lemma |
|
388 fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)" |
|
389 shows "(p \<bullet> (P The)) = foo" |
|
390 apply(perm_simp exclude: The) |
|
391 oops |
|
392 |
387 thm eqvts |
393 thm eqvts |
388 thm eqvts_raw |
394 thm eqvts_raw |
389 |
395 |
390 ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *} |
396 ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *} |
391 |
397 |