theory Classical
imports "../NewParser"
begin

(* example from my Urban's PhD *)

atom_decl name
atom_decl coname

declare [[STEPS = 21]]

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

thm distinct
thm induct
thm exhaust
thm fv_defs
thm bn_defs
thm perm_simps
thm eq_iff
thm fv_bn_eqvt
thm size_eqvt




end