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的），等等。只是看看菜單，找出更多。我試圖盡量減少非伊莎貝爾特定軟件的數量，以減少下載大小。
什麼是新的，在此版本：