关于AFP依赖查询工具及Jacobson_Basic_Algebra域论扩展的问询

一、查找AFP中依赖特定程序包的工具 #

• AFP官网内置功能：每个AFP条目页面都有「Dependencies」和「Reverse Dependencies」板块，前者展示该包依赖的其他条目，后者展示哪些条目依赖它，直接就能查询目标包的被依赖情况。
• Isabelle脚本分析：可以用Isabelle自带的ML脚本批量遍历AFP库的理论文件，提取依赖关系；也可借助find_theorems等命令辅助定位依赖关联的理论内容。
• 社区工具：部分社区维护的Isabelle依赖可视化工具，能生成直观的依赖图谱，帮助梳理包之间的依赖链。

二、Jacobson_Basic_Algebra的域论方向扩展 #

目前AFP中直接基于Jacobson_Basic_Algebra做域论专项扩展的条目较少，但可以从以下方向入手：

• 相关代数条目复用：涉及域扩张、伽罗瓦理论的AFP条目，不少会复用Jacobson_Basic_Algebra中的基础代数结构定义，可重点关注这类内容。
• 域论分类条目：查看AFP中「Field Theory」分类下的条目，部分条目兼容Jacobson_Basic_Algebra的框架，你也可以基于它的基础理论进行自定义扩展。

内容的提问来源于stack exchange，提问作者alagris