diff -r 419116f1157a -r e23770bc97c8 src/HOL/AxClasses/Product.thy --- a/src/HOL/AxClasses/Product.thy Thu Feb 26 08:44:44 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