Linear and non-linear types: Types.thy, Types.ML.
Linear and non-linear types: Types.thy, Types.ML.
Untyped environments: Env.thy, Env.ML.
Typed environments: TypedEnv.thy, TypedEnv.ML.
The meta language: Meta.thy, Meta.ML.
The typed meta language: TypedMeta.thy, TypedMeta.ML.
Substitution: Subst.thy, Subst.ML.
The linear pi calculus: Pi.thy, Pi.ML.
Additional tactics: Tactics.thy, Tactics.ML.