| changeset 12338 | de0f4a63baa5 |
| parent 10681 | ec76e17f73c5 |
| child 14981 | e73f8140af78 |
| 12337:7c6a970f0808 | 12338:de0f4a63baa5 |
|---|---|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 *) |
5 *) |
6 |
6 |
7 theory Product = Main: |
7 theory Product = Main: |
8 |
8 |
9 axclass product < "term" |
9 axclass product < type |
10 |
10 |
11 consts |
11 consts |
12 product :: "'a::product => 'a => 'a" (infixl "[*]" 70) |
12 product :: "'a::product => 'a => 'a" (infixl "[*]" 70) |
13 |
13 |
14 |
14 |