# HG changeset patch
# User nipkow
# Date 1268670843 -3600
# Node ID 3c1601857a6b033ca3f5917a8417be185377848a
# Parent  533dd944e29ca70d049a0dcae76c4869323b1d2c# Parent  362431732b5e9d73d42054fa9e3701f71ce8e94f
merged

diff -r 362431732b5e -r 3c1601857a6b src/HOL/Finite_Set.thy
--- 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 *}
diff -r 362431732b5e -r 3c1601857a6b src/HOL/Library/Library/document/root.tex
--- 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}