# HG changeset patch
# User wenzelm
# Date 1618862272 -7200
# Node ID c642c3cbbf0eefa3cf892e5ac2144120b86abbc4
# Parent  c1f8aaa13ee3c6ef0d9c54f0cef9028e242ffd1c
more documentation on "Conversions";

diff -r c1f8aaa13ee3 -r c642c3cbbf0e src/Doc/Implementation/Eq.thy
--- a/src/Doc/Implementation/Eq.thy	Mon Apr 19 15:55:14 2021 +0200
+++ b/src/Doc/Implementation/Eq.thy	Mon Apr 19 21:57:52 2021 +0200
@@ -74,10 +74,27 @@
 section \<open>Conversions \label{sec:conv}\<close>
 
 text \<open>
-  %FIXME
+  The classic article @{cite "paulson:1983"} introduces the concept of
+  conversion for Cambridge LCF. This was historically important to implement
+  all kinds of ``simplifiers'', but the Isabelle Simplifier is done quite
+  differently, see @{cite \<open>\S9.3\<close> "isabelle-isar-ref"}.
+\<close>
 
-  The classic article that introduces the concept of conversion (for Cambridge
-  LCF) is @{cite "paulson:1983"}.
+text %mlref \<open>
+  \begin{mldecls}
+  @{index_ML_structure Conv} \\
+  @{index_ML_type conv} \\
+  @{index_ML Simplifier.asm_full_rewrite : "Proof.context -> conv"} \\
+  \end{mldecls}
+
+  \<^descr> \<^ML_structure>\<open>Conv\<close> is a library of combinators to build conversions,
+  over type \<^ML_type>\<open>conv\<close> (see also \<^file>\<open>~~/src/Pure/conv.ML\<close>). This is one
+  of the few Isabelle/ML modules that are usually used with \<^verbatim>\<open>open\<close>: finding
+  examples works by searching for ``\<^verbatim>\<open>open Conv\<close>'' instead of ``\<^verbatim>\<open>Conv.\<close>''.
+
+  \<^descr> \<^ML>\<open>Simplifier.asm_full_rewrite\<close> invokes the Simplifier as a
+  conversion. There are a few related operations, corresponding to the various
+  modes of simplification.
 \<close>