IsaMorph

IsaMorph是一个Linux发行版的Live CD（基于Morphix）为特色的交互式定理证明伊莎贝尔。
这意味着，你可以从光盘启动，并得到一个全面运作的“定理证明”的环境中，无需安装GNU / Linux或伊莎贝尔。只需插入光盘放入电脑，并有五分钟后你的第一个定理的证明。
在IsaMorph分布的所有程序都是免费的软件。这意味着，操作系统和包含在该光盘中的应用程序可以自由地复制，修改和分发。所以，请随时给副本给你的朋友或同事。
将CD插入一个Intel兼容PC或笔记本电脑上的CD驱动器。现在，重新启动计算机。确保第一启动设备为CD。对于这一点，您可能需要更改计算机的BIOS设置。
如果你不熟悉它，从你的系统管理员或某人谁知道如何做到这一点帮助。在计算机启动时启动，它将搜索驱动器的CD。一段时间后，会出现一个菜单。
只要按下回车键或等待一段时间。计算机将继续从光盘启动，并有望给您类似于你熟悉的图形界面。您可以在左上角点击菜单和启动应用程序。
IsaMorph包含一个完整的工作环境伊莎贝尔支持证明和文档生成，这包括：
伊莎贝尔（2005年版）
交互式定理证明2005年与伊莎贝尔至少在编译如下逻辑：HOL，HOL-复杂，采埃孚，FOL，纯净。因此，启动后IsaMorph可以立即证明定理在任何这些逻辑的。该光盘包括伊莎贝尔的教程和理论文档一个离线版本。
HOL-TestGen（1.1.1版）
测试用例生成基于规范的单元测试。它是建立在specfication和定理证明环境伊莎贝尔/ HOL的顶部。
一般证明（版本3.6pre）
强大的用户界面的伊莎贝尔。
新泽西州的SML（版本110.56）
标准ML环境用于编译和执行伊莎贝尔。
GNU Emacs的（22.0.50版）
GNU Emacs编辑器它与一般的证明伊莎贝尔的主要用户界面结合在一起生成。
teTeX系统（版本2.0.2）
用于证明文件的生成一个完整的LaTeX的环境。
其他应用程序
此外，该光盘还包含了各种为共同使用的应用程序。它包括一个用户友好的桌面（侏儒）互联网浏览器（Mozilla的），等等。只是看看菜单，找出更多。我试图尽量减少非伊莎贝尔特定软件的数量，以减少下载大小。
什么是新的，在此版本：