8.3 Type Classes 型クラスの概念はHaskellによって広まりました。型クラスは型とインタフェースの集合を定義し、そのクラスに属する型はインタフェースを実装しなければなりません。Isabelleが提供する型クラスも同様ですが、さらにプロパティ(型公理)を定…