equal
deleted
inserted
replaced
52 This is done for class $product$ and type $bool$ as follows. |
52 This is done for class $product$ and type $bool$ as follows. |
53 *} |
53 *} |
54 |
54 |
55 instance bool :: product |
55 instance bool :: product |
56 by intro_classes |
56 by intro_classes |
57 defs |
57 defs (overloaded) |
58 product_bool_def: "x \\<Otimes> y \\<equiv> x \\<and> y" |
58 product_bool_def: "x \\<Otimes> y \\<equiv> x \\<and> y" |
59 |
59 |
60 text {* |
60 text {* |
61 The definition $prod_bool_def$ becomes syntactically well-formed only |
61 The definition $prod_bool_def$ becomes syntactically well-formed only |
62 after the arity $bool :: product$ is made known to the type checker. |
62 after the arity $bool :: product$ is made known to the type checker. |