--- a/src/HOL/Induct/Mutil.thy Tue May 02 18:54:59 2000 +0200
+++ b/src/HOL/Induct/Mutil.thy Tue May 02 18:55:11 2000 +0200
@@ -27,6 +27,6 @@
"below n == {i. i<n}"
colored :: "nat => (nat*nat)set"
- "colored b == {(i,j). (i+j) mod 2 = b}"
+ "colored b == {(i,j). (i+j) mod #2 = b}"
end