# HG changeset patch
# User wenzelm
# Date 1287687973 -3600
# Node ID 1206e88f1284ff9d082e82cf404c4f1efa4152c4
# Parent  1ff9bce085bd49410b0f46b15cd1050024597760
more refs;

diff -r 1ff9bce085bd -r 1206e88f1284 doc-src/IsarImplementation/Thy/Local_Theory.thy
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Thu Oct 21 20:00:46 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Thu Oct 21 20:06:13 2010 +0100
@@ -156,6 +156,9 @@
 
 section {* Morphisms and declarations \label{sec:morphisms} *}
 
-text FIXME
+text {* FIXME
+
+  \medskip See also \cite{Chaieb-Wenzel:2007}.
+*}
 
 end
diff -r 1ff9bce085bd -r 1206e88f1284 doc-src/manual.bib
--- a/doc-src/manual.bib	Thu Oct 21 20:00:46 2010 +0100
+++ b/doc-src/manual.bib	Thu Oct 21 20:06:13 2010 +0100
@@ -319,6 +319,18 @@
 
 %C
 
+@InProceedings{Chaieb-Wenzel:2007,
+  author = 	 {Amine Chaieb and Makarius Wenzel},
+  title = 	 {Context aware Calculation and Deduction ---
+                  Ring Equalities via {Gr\"obner Bases} in {Isabelle}},
+  booktitle =	 {Towards Mechanized Mathematical Assistants (CALCULEMUS 2007)},
+  editor =	 {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger},
+  series =	 LNAI,
+  volume =       4573,
+  year =	 2007,
+  publisher =	 Springer
+}
+
 @TechReport{camilleri92,
   author	= {J. Camilleri and T. F. Melham},
   title		= {Reasoning with Inductively Defined Relations in the