author | wenzelm |
Sat, 27 Oct 2001 00:09:59 +0200 | |
changeset 11963 | a6608d44a46b |
parent 10681 | ec76e17f73c5 |
child 12338 | de0f4a63baa5 |
permissions | -rw-r--r-- |
(* Title: HOL/AxClasses/Product.thy ID: $Id$ Author: Markus Wenzel, TU Muenchen License: GPL (GNU GENERAL PUBLIC LICENSE) *) theory Product = Main: axclass product < "term" consts product :: "'a::product => 'a => 'a" (infixl "[*]" 70) instance bool :: product by intro_classes defs (overloaded) product_bool_def: "x [*] y == x & y" end