doc-src/IsarAdvanced/Classes/Thy/Classes.thy
changeset 27503 a019d6568a3c
parent 27189 1a9b9da1c0d7
child 27504 5287623e7ff9
equal deleted inserted replaced
27502:a8561998cea7 27503:a019d6568a3c
    65 
    65 
    66   \medskip\noindent\hspace*{2ex}@{text "class ord extends eq where"} \\
    66   \medskip\noindent\hspace*{2ex}@{text "class ord extends eq where"} \\
    67   \hspace*{4ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
    67   \hspace*{4ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
    68   \hspace*{4ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
    68   \hspace*{4ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
    69 
    69 
    70   \medskip\noindent Type variables are annotated with (finitly many) classes;
    70   \medskip\noindent Type variables are annotated with (finitely many) classes;
    71   these annotations are assertions that a particular polymorphic type
    71   these annotations are assertions that a particular polymorphic type
    72   provides definitions for overloaded functions.
    72   provides definitions for overloaded functions.
    73 
    73 
    74   Indeed, type classes not only allow for simple overloading
    74   Indeed, type classes not only allow for simple overloading
    75   but form a generic calculus, an instance of order-sorted
    75   but form a generic calculus, an instance of order-sorted