diff -r c50fc8023ac0 -r a7f961fb62c6 doc-src/AxClass/Group/Product.thy
--- a/doc-src/AxClass/Group/Product.thy	Mon Oct 23 22:09:52 2000 +0200
+++ b/doc-src/AxClass/Group/Product.thy	Mon Oct 23 22:10:36 2000 +0200
@@ -41,8 +41,7 @@
  Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the
  type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
  type signature.  In our example, this arity may be always added when
- required by means of an $\INSTANCE$ with the trivial proof
- $\BY{intro_classes}$.
+ required by means of an $\INSTANCE$ with the default proof $\DDOT$.
 
  \medskip Thus, we may observe the following discipline of using
  syntactic classes.  Overloaded polymorphic constants have their type
@@ -54,8 +53,7 @@
  follows.
 *}
 
-instance bool :: product
-  by intro_classes
+instance bool :: product ..
 defs (overloaded)
   product_bool_def: "x \<odot> y \<equiv> x \<and> y"