Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
defs (overloaded);
authorwenzelm
Sun, 16 Jul 2000 20:54:38 +0200
changeset 9363 86b48eafc70d
parent 9362 b78d4246a320
child 9364 e783491b9a1f
defs (overloaded);
src/HOL/AxClasses/Tutorial/Group.thy file | annotate | diff | comparison | revisions
src/HOL/AxClasses/Tutorial/Product.thy file | annotate | diff | comparison | revisions 
--- 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;
--- 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;
isabelle