| changeset 29748 | 2ff24d87fad1 |
| parent 29747 | bab2371e0348 |
| child 29749 | 5a576282c935 |
| 29747:bab2371e0348 | 29748:2ff24d87fad1 |
|---|---|
1 (* Title: HOL/AxClasses/Product.thy |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 *) |
|
5 |
|
6 theory Product imports Main begin |
|
7 |
|
8 axclass product < type |
|
9 |
|
10 consts |
|
11 product :: "'a::product => 'a => 'a" (infixl "[*]" 70) |
|
12 |
|
13 |
|
14 instance bool :: product |
|
15 by intro_classes |
|
16 |
|
17 defs (overloaded) |
|
18 product_bool_def: "x [*] y == x & y" |
|
19 |
|
20 end |