| changeset 16417 | 9bc16273c2d4 |
| parent 14981 | e73f8140af78 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 (* Title: HOL/AxClasses/Product.thy |
1 (* Title: HOL/AxClasses/Product.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 theory Product = Main: |
6 theory Product imports Main begin |
7 |
7 |
8 axclass product < type |
8 axclass product < type |
9 |
9 |
10 consts |
10 consts |
11 product :: "'a::product => 'a => 'a" (infixl "[*]" 70) |
11 product :: "'a::product => 'a => 'a" (infixl "[*]" 70) |