这是 hol-light 命令，可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行，例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序：
您的姓名
hol-light - HOL Light 交互式定理证明器
概要
全光 [选项...]
商品描述
命令 全光 是一个简单的调用包装器 卡姆 并加载 HOL Light
基本定义（通过加载 /usr/share/hol-light/hol.ml 而不是 .ocamlinit as
初始化文件）。 在现代硬件上加载这些定义大约需要 2 分钟，
请耐心等待。 所有选项和其他参数都作为选项传递给 卡姆.
如果你有一个 阅读编辑器 如 包装纸, 领导 or 费 安装好了 全光 卡姆
顶层被包裹在 阅读编辑器. 仅安装这些 readline 编辑器之一或
通过替代系统配置您的首选。
使用 onworks.net 服务在线使用 hol-light
