theory Classical
imports "../NewParser"
begin

(* example from my Urban's PhD *)

atom_decl name
atom_decl coname

declare [[STEPS = 9]]

nominal_datatype trm =
   Ax "name" "coname"
|  Cut n::"coname" t1::"trm" c::"coname" t2::"trm"              bind_set n in t1, bind_set c in t2
|  AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname"  bind_set c1 in t1, bind_set c2 in t2
|  AndL1 n::"name" t::"trm" "name"                              bind_set n in t
|  AndL2 n::"name" t::"trm" "name"                              bind_set n in t
|  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"        bind_set c in t1, bind_set n in t2
|  ImpR c::"coname" n::"name" t::"trm" "coname"                 bind_set n c in t

thm alpha_trm_raw.intros[no_vars]

(*
thm trm.fv
thm trm.eq_iff
thm trm.bn
thm trm.perm
thm trm.induct
thm trm.distinct
thm trm.fv[simplified trm.supp]
*)


end