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