"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
theory LF
imports "../NewParser"
begin
declare [[STEPS = 100]]
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" ty::"ty" bind n in ty
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