# HG changeset patch
# User haftmann
# Date 1706789697 0
# Node ID 82fbd5919f2424638dbb39a6670af9e575f5e009
# Parent  33b10cd883ae8992c44cb17e6acb5099118958c7
explicit reference to code_dt

diff -r 33b10cd883ae -r 82fbd5919f24 src/Doc/Codegen/Refinement.thy
--- a/src/Doc/Codegen/Refinement.thy	Thu Feb 01 17:06:40 2024 +0100
+++ b/src/Doc/Codegen/Refinement.thy	Thu Feb 01 12:14:57 2024 +0000
@@ -265,6 +265,9 @@
 \<close>
 
 text \<open>
+  To reduce manual work for datatype refinement, @{command_def lift_definition}
+  is a valuable tool.  See the corresponding section in \<^cite>\<open>"isabelle-isar-ref"\<close>.
+
   See further \<^cite>\<open>"Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement"\<close>
   for the meta theory of datatype refinement involving invariants.