在伊莎贝尔的NEWS档案中，我发现
\n\n\n命令“typedef”现在在本地理论上下文中工作——无需引入对参数或假设的依赖，而这在 Isabelle/Pure/HOL 中是不可能的。请注意，即使在全局理论上下文中，逻辑环境也可能包含局部 typedef 的多种解释（具有不同的非空性证明）。
\n
（可以追溯到 Isabelle2009-2）。这是关于typedef当地理论背景的最新消息吗？此外，“不引入对参数或假设的依赖”的限制实际上意味着什么？
如果这意味着我不能在 a 的定义集中使用区域设置参数typedef，那么我根本不会考虑typedef本地化（因为唯一允许的实例可以轻松地移到本地上下文之外，或者我是否遗漏了某些内容？）。
是否（或者应该，或者将会）可以沿着线做一些事情（其中用于 a 的集合取决于typedeflocale 参数V）：
datatype (\'a, \'b) "term" = Var \'b | Fun \'a "(\'a, \'b) term list"\n\nlocale term_algebra =\n fixes F :: "\'a set"\n and V :: "\'b set"\nbegin\n\ndefinition "domain \xce\xb1 = {x : V. \xce\xb1 x ~= Var x}"\n\ntypedef (\'a, \'b) subst =\n "{\xce\xb1 :: \'b => (\'a, \'b) term. finite (domain \xce\xb1)}"\n\nend\n我目前获得的：
\n\nLocally fixed type arguments "\'a", "\'b" in type declaration "subst"\n对此还有一些注意事项：
本地理论基础设施仅仅组织现有的模块概念（locale等）class，使得定义机制（definition、theorem、等）可以在各种上下文中统一工作。这不会改变逻辑基础，因此不能依赖项参数 ( ) 或前提 ( ) 的规范元素不会从根本上变得更好。它们只是被改装成更大的框架，这已经是一个超逻辑的好处。inductivefunctionfixesassumes
规范的局部理论目标是locale及其衍生物，例如class。这些在根据上面概述的原理的逻辑中工作：通过fixes和的某些上下文进行 lambda 提升assumes。其他更雄心勃勃的目标是可以想象的，但需要一些勇敢的英雄人物来实现。例如，人们可以将AWE理论解释机制包装为另一个本地理论目标，然后获得类型/常量/公理的参数化——通常的成本是通过显式证明术语来在 LCF 证明者中实现可接受的推论（或者以放弃 LCF 性为代价并通过某些预言机来实现）。
正如上面所描绘的那样， Plain typedef（及其衍生品，如本地化codatatype和datatype最近的 HOL-BNF）可以在其依赖类型参数方面略有改进，但这意味着一些实现工作并不能证明目前的微薄结果是合理的。它只允许使用隐式参数编写多态类型构造，如下所示：
context fixes type 'a
begin
datatype list = Nil | Cons 'a list
end
导出后你会'a list像往常一样得到。
进一步的复杂化：fixes type 'a不存在。Isabelle/Pure 通过 Hindley-Milner 隐式处理类型参数。