changeset 7800 | 8ee919e42174 |
parent 7761 | 7fab9592384f |
child 7874 | 180364256231 |
--- a/src/HOL/Isar_examples/Group.thy Fri Oct 08 15:08:47 1999 +0200 +++ b/src/HOL/Isar_examples/Group.thy Fri Oct 08 15:09:14 1999 +0200 @@ -11,7 +11,8 @@ text {* We define an axiomatic type class of general groups over signature - $({\times}, \idt{one}, \idt{inv})$. + $({\times} :: \alpha \To \alpha \To \alpha, \idt{one} :: \alpha, + \idt{inv} :: \alpha \To \alpha)$. *}; consts