author | haftmann |
Mon, 11 Aug 2008 14:50:00 +0200 | |
changeset 27824 | 97d2a3797ce0 |
parent 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
(* Title: HOL/AxClasses/Product.thy ID: $Id$ Author: Markus Wenzel, TU Muenchen *) theory Product imports Main begin axclass product < type consts product :: "'a::product => 'a => 'a" (infixl "[*]" 70) instance bool :: product by intro_classes defs (overloaded) product_bool_def: "x [*] y == x & y" end