# HG changeset patch
# User wenzelm
# Date 963773678 -7200
# Node ID 86b48eafc70d23fed6caa77db79b38f3ca1fd334
# Parent  b78d4246a320631d122ac02d44b2590c9078be3c
defs (overloaded);

diff -r b78d4246a320 -r 86b48eafc70d src/HOL/AxClasses/Tutorial/Group.thy
--- a/src/HOL/AxClasses/Tutorial/Group.thy	Sun Jul 16 20:54:24 2000 +0200
+++ b/src/HOL/AxClasses/Tutorial/Group.thy	Sun Jul 16 20:54:38 2000 +0200
@@ -94,7 +94,7 @@
 
 subsection {* Concrete instantiation *};
 
-defs
+defs (overloaded)
   times_bool_def:   "x [*] y == x ~= (y::bool)"
   inverse_bool_def: "inverse x == x::bool"
   unit_bool_def:    "one == False";
@@ -112,7 +112,7 @@
 
 subsection {* Lifting and Functors *};
 
-defs
+defs (overloaded)
   times_prod_def: "p [*] q == (fst p [*] fst q, snd p [*] snd q)";
 
 instance * :: (semigroup, semigroup) semigroup;
diff -r b78d4246a320 -r 86b48eafc70d src/HOL/AxClasses/Tutorial/Product.thy
--- 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;