changeset 30130 | e23770bc97c8 |
parent 30129 | 419116f1157a |
parent 30114 | 0726792e1726 |
child 30131 | 6be1be402ef0 |
--- 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