src/HOL/AxClasses/Tutorial/Product.thy
changeset 9363 86b48eafc70d
parent 8920 af5e09b6c208
child 10007 64bf7da1994a
--- a/src/HOL/AxClasses/Tutorial/Product.thy	Sun Jul 16 20:54:24 2000 +0200
+++ b/src/HOL/AxClasses/Tutorial/Product.thy	Sun Jul 16 20:54:38 2000 +0200
@@ -12,7 +12,7 @@
 
 instance bool :: product;
   by intro_classes;
-defs
+defs (overloaded)
   product_bool_def: "x [*] y == x & y";
 
 end;