--- a/src/HOL/Finite_Set.thy Mon Mar 15 17:33:41 2010 +0100
+++ b/src/HOL/Finite_Set.thy Mon Mar 15 17:34:03 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 *}
--- a/src/HOL/Library/Library/document/root.tex Mon Mar 15 17:33:41 2010 +0100
+++ b/src/HOL/Library/Library/document/root.tex Mon Mar 15 17:34:03 2010 +0100
@@ -2,7 +2,7 @@
\usepackage{ifthen}
\usepackage[latin1]{inputenc}
\usepackage[english]{babel}
-\usepackage{isabelle,isabellesym,amssymb}
+\usepackage{isabelle,isabellesym,amssymb,stmaryrd}
\usepackage{pdfsetup}
\urlstyle{rm}