src/HOL/Isar_examples/Group.thy
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