equal
deleted
inserted
replaced
1 (* Title: HOL/AxClasses/Tutorial/Product.thy |
1 (* Title: HOL/AxClasses/Tutorial/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 = Main: |
7 |
7 |
8 axclass |
8 axclass |
9 product < "term"; |
9 product < "term" |
10 consts |
10 consts |
11 product :: "'a::product => 'a => 'a" (infixl "[*]" 70); |
11 product :: "'a::product => 'a => 'a" (infixl "[*]" 70) |
12 |
12 |
13 instance bool :: product; |
13 instance bool :: product |
14 by intro_classes; |
14 by intro_classes |
15 defs (overloaded) |
15 defs (overloaded) |
16 product_bool_def: "x [*] y == x & y"; |
16 product_bool_def: "x [*] y == x & y" |
17 |
17 |
18 end; |
18 end |