theory Classicalimports "../Nominal2"begin(* example from Urban's PhD *)atom_decl nameatom_decl conamenominal_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 tthm trm.distinctthm trm.inductthm trm.exhaustthm trm.strong_exhaustthm trm.strong_exhaust[simplified]thm trm.fv_defsthm trm.bn_defsthm trm.perm_simpsthm trm.eq_iffthm trm.fv_bn_eqvtthm trm.size_eqvtthm trm.suppthm trm.supp[simplified]end