author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 10681 | ec76e17f73c5 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
10134 | 1 |
(* Title: HOL/AxClasses/Product.thy |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
10681 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
10134 | 5 |
*) |
6 |
||
7 |
theory Product = Main: |
|
8 |
||
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
10681
diff
changeset
|
9 |
axclass product < type |
10134 | 10 |
|
11 |
consts |
|
12 |
product :: "'a::product => 'a => 'a" (infixl "[*]" 70) |
|
13 |
||
14 |
||
15 |
instance bool :: product |
|
16 |
by intro_classes |
|
17 |
||
18 |
defs (overloaded) |
|
19 |
product_bool_def: "x [*] y == x & y" |
|
20 |
||
21 |
end |