| changeset 8920 | af5e09b6c208 |
| parent 8919 | d00b01ed8539 |
| child 8921 | 7c04c98132c4 |
| 8919:d00b01ed8539 | 8920:af5e09b6c208 |
|---|---|
1 (* Title: HOL/AxClasses/Tutorial/Sigs.thy |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 Some polymorphic constants for the 'signature' parts of axclasses. |
|
6 *) |
|
7 |
|
8 Sigs = HOL + |
|
9 |
|
10 consts |
|
11 "<*>" :: "['a, 'a] => 'a" (infixl 70) |
|
12 inverse :: "'a => 'a" |
|
13 "1" :: "'a" ("1") |
|
14 |
|
15 end |