moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
theory ExLF
imports "../Parser"
begin
atom_decl name
atom_decl ident
nominal_datatype kind =
Type
| KPi "ty" n::"name" k::"kind" bind n in k
and ty =
TConst "ident"
| TApp "ty" "trm"
| TPi "ty" n::"name" t::"ty" bind n in t
and trm =
Const "ident"
| Var "name"
| App "trm" "trm"
| Lam "ty" n::"name" t::"trm" bind n in t
thm kind_ty_trm.supp
end