--- a/src/HOL/Finite_Set.thy Sun Mar 14 19:48:33 2010 -0700
+++ b/src/HOL/Finite_Set.thy Mon Mar 15 15:13:07 2010 +0100
@@ -1586,8 +1586,8 @@
end
-no_notation (in times) times (infixl "*" 70)
-no_notation (in one) Groups.one ("1")
+no_notation times (infixl "*" 70)
+no_notation Groups.one ("1")
locale folding_image_simple = comm_monoid +
fixes g :: "('b \<Rightarrow> 'a)"
@@ -1742,8 +1742,8 @@
end
-notation (in times) times (infixl "*" 70)
-notation (in one) Groups.one ("1")
+notation times (infixl "*" 70)
+notation Groups.one ("1")
subsection {* Finite cardinality *}