--- 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
--- 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