Isabelle2016でタイプインポートが動作していないようです

Question

私はIsabelleの初心者です。次の一見単純なテストコードはコンパイルできません：

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

    thm inner_zero_left 
    typ "real_inner" 
end 

jeditインターフェイスでは、thmコマンドが正常に動作しているように見えます（Inner_Productのインポートでは定理が見えます）が、real_inner typは正しくありません。それは不平を言っています

私は定理でreal_innerを使用しようとすると同じエラーが発生します。

Answer 1

real_innerは型ではありません。これは型クラスです。 '型の種類real_inner'を意味する場合は、ソートアノテーション付きフリータイプの変数real_innerを使用する必要があります。