theory SingleLetimports "../NewParser"beginatom_decl namedeclare [[STEPS = 16]]nominal_datatype trm = Var "name"| App "trm" "trm"| Lam x::"name" t::"trm" bind_set x in t| Let a::"assg" t::"trm" bind_set "bn a" in t| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2| Bar x::"name" y::"name" t::"trm" bind y x in t x y| Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 and assg = As "name" x::"name" t::"trm" bind x in tbinder bn::"assg \<Rightarrow> atom set"where "bn (As x y t) = {atom x}"term Var term Appterm Bazterm bnterm fv_trmtyp trmtyp assgthm trm_assg.fvthm trm_assg.suppthm trm_assg.eq_iffthm trm_assg.bnthm trm_assg.permthm trm_assg.inductthm trm_assg.inductsthm trm_assg.distinctML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}(* TEMPORARYthm trm_assg.fv[simplified trm_assg.supp(1-2)]*)end