| author | wenzelm |
| Thu, 17 Aug 2000 10:37:04 +0200 | |
| changeset 9624 | de254f375477 |
| parent 9363 | 86b48eafc70d |
| child 10007 | 64bf7da1994a |
| permissions | -rw-r--r-- |
(* Title: HOL/AxClasses/Tutorial/Product.thy ID: $Id$ Author: Markus Wenzel, TU Muenchen *) theory Product = Main:; axclass product < "term"; consts product :: "'a::product => 'a => 'a" (infixl "[*]" 70); instance bool :: product; by intro_classes; defs (overloaded) product_bool_def: "x [*] y == x & y"; end;