| changeset 1247 | 18b1441fb603 |
| 1246:706cfddca75c | 1247:18b1441fb603 |
|---|---|
1 (* Title: HOL/AxClasses/Tutorial/ProductInsts.thy |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 Instantiate the 'syntactic' class "product", then define "<*>" on type |
|
6 "bool". |
|
7 |
|
8 Note: This may look like Haskell-instance, but is not quite the same! |
|
9 *) |
|
10 |
|
11 ProductInsts = Product + |
|
12 |
|
13 instance |
|
14 bool :: product |
|
15 |
|
16 defs |
|
17 prod_bool_def "x <*> y == x & y::bool" |
|
18 |
|
19 end |