src/HOL/AxClasses/Tutorial/ProductInsts.thy
changeset 8920 af5e09b6c208
parent 8919 d00b01ed8539
child 8921 7c04c98132c4
--- a/src/HOL/AxClasses/Tutorial/ProductInsts.thy	Mon May 22 13:20:47 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      HOL/AxClasses/Tutorial/ProductInsts.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Instantiate the 'syntactic' class "product", then define "<*>" on type
-"bool".
-
-Note: This may look like Haskell-instance, but is not quite the same!
-*)
-
-ProductInsts = Product +
-
-instance
-  bool :: product
-
-defs
-  prod_bool_def "x <*> y  == x & y::bool"
-
-end