equal
deleted
inserted
replaced
1289 in @{ML_file "Pure/unify.ML"}. It uses lazy sequences which are implemented |
1289 in @{ML_file "Pure/unify.ML"}. It uses lazy sequences which are implemented |
1290 in @{ML_file "Pure/General/seq.ML"}. |
1290 in @{ML_file "Pure/General/seq.ML"}. |
1291 \end{readmore} |
1291 \end{readmore} |
1292 *} |
1292 *} |
1293 |
1293 |
1294 section {* Sorts (TBD) *} |
1294 section {* Sorts (TBD)\label{sec:sorts} *} |
1295 |
1295 |
1296 text {* |
1296 text {* |
1297 Type classes are formal names in the type system which are linked to |
1297 Type classes are formal names in the type system which are linked to |
1298 predicates of one type variable (via the axclass mechanism) and thereby |
1298 predicates of one type variable (via the axclass mechanism) and thereby |
1299 express extra properties on types, to be propagated by the type system. |
1299 express extra properties on types, to be propagated by the type system. |