changeset 30105 | 37f47ea6fed1 |
parent 30104 | b094999e1d33 |
parent 30101 | 5c6efec476ae |
child 30106 | 351fc2f8493d |
--- a/src/HOL/AxClasses/Product.thy Thu Feb 26 06:39:06 2009 -0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ -(* 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