equal
deleted
inserted
replaced
747 (*<*) |
747 (*<*) |
748 setup {* Sign.add_path "foo" *} |
748 setup {* Sign.add_path "foo" *} |
749 consts "op =" :: "'a" |
749 consts "op =" :: "'a" |
750 (*>*) |
750 (*>*) |
751 |
751 |
752 axclass eq \<subseteq> type |
752 class eq (attach "op =") = notes reflexive |
753 (attach "op =") |
|
754 |
753 |
755 text {* |
754 text {* |
756 This merely introduces a class @{text eq} with corresponding |
755 This merely introduces a class @{text eq} with corresponding |
757 operation @{text "op ="}; |
756 operation @{text "op ="}; |
758 the preprocessing framework does the rest. |
757 the preprocessing framework does the rest. |