--- a/doc-src/Codegen/Thy/document/Refinement.tex Tue Feb 21 12:45:00 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Tue Feb 21 13:10:13 2012 +0100
@@ -628,9 +628,9 @@
%
\begin{isamarkuptext}%
Typical data structures implemented by representations involving
- invariants are available in the library, theory \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}}
+ invariants are available in the library, theory \isa{Mapping}
specifies key-value-mappings (type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ mapping});
- these can be implemented by red-black-trees (theory \hyperlink{theory.RBT}{\mbox{\isa{RBT}}}).%
+ these can be implemented by red-black-trees (theory \isa{RBT}).%
\end{isamarkuptext}%
\isamarkuptrue%
%