theory TestMorePerm
imports "../Parser"
begin

text {* weirdo example from Peter Sewell's bestiary *}

nominal_datatype weird =
  WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
    bind x in p1, bind x in p2, bind y in p2, bind y in p3
| WV "name"
| WP "weird" "weird"

thm permute_weird_raw.simps[no_vars]
thm alpha_weird_raw.intros[no_vars]
thm fv_weird_raw.simps[no_vars]


end