changeset 1247 | 18b1441fb603 |
child 2907 | 0e272e4c7cb2 |
1246:706cfddca75c | 1247:18b1441fb603 |
---|---|
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 "inv" :: "'a => 'a" |
|
13 "1" :: "'a" ("1") |
|
14 |
|
15 end |