src/HOL/AxClasses/Product.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 16417 9bc16273c2d4
permissions -rw-r--r--
simplified code generator setup
     1 (*  Title:      HOL/AxClasses/Product.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 theory Product imports Main begin
     7 
     8 axclass product < type
     9 
    10 consts
    11   product :: "'a::product => 'a => 'a"    (infixl "[*]" 70)
    12 
    13 
    14 instance bool :: product
    15   by intro_classes
    16 
    17 defs (overloaded)
    18   product_bool_def: "x [*] y == x & y"
    19 
    20 end