类型导入似乎并没有为我工作在Isabelle2016

我是一个完整的初学者Isabelle，我必须做错了，因为下面看似简单的测试代码只是不编译我：类型导入似乎并没有为我工作在Isabelle2016

theory testit 
imports 
    "~~/src/HOL/Library/Inner_Product" 
begin 

    thm inner_zero_left 
    typ "real_inner" 
end

在jedit界面中，thm命令似乎工作正常（所以它在Inner_Product导入中看到了定理），但real_inner类型不是。这是抱怨

Undefined type name: "real_inner"⌂ 
Failed to parse type

我得到同样的错误，如果我尝试在定理中使用real_inner。

real_inner不是一种类型;这是一个类型类。如果您的意思是'一种类型类型real_inner'，则需要使用带排序注释的自由类型变量real_inner：

typ "'a :: real_inner"

2016-10-31 12:27:00

回答