# HG changeset patch
# User wenzelm
# Date 1266614970 -3600
# Node ID 024fef37a65d97b9a392a706105b2f24c331491b
# Parent  1c80c29086d74ad1e3c0f71f30f743fa6c676f1b
fixed document;

diff -r 1c80c29086d7 -r 024fef37a65d src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Fri Feb 19 22:25:26 2010 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy	Fri Feb 19 22:29:30 2010 +0100
@@ -24,7 +24,7 @@
 declare [[map "+" = (sum_map, sum_rel)]]
 
 
-text {* should probably be in Sum_Type.thy *}
+text {* should probably be in @{theory Sum_Type} *}
 lemma split_sum_all:
   shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
   apply(auto)