src/HOL/AxClasses/Product.thy
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