diff -r d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/ProductInsts.thy --- 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