# HG changeset patch
# User haftmann
# Date 1502520986 -7200
# Node ID 82e2291cabff19c483283f22548b333323a99e56
# Parent  7eb451adbda62c16e80b28f12161d32d4e230708
be more explicit on type dlist

diff -r 7eb451adbda6 -r 82e2291cabff src/Doc/Codegen/Refinement.thy
--- a/src/Doc/Codegen/Refinement.thy	Sat Aug 12 08:56:25 2017 +0200
+++ b/src/Doc/Codegen/Refinement.thy	Sat Aug 12 08:56:26 2017 +0200
@@ -184,12 +184,15 @@
 text \<open>
   Datatype representation involving invariants require a dedicated
   setup for the type and its primitive operations.  As a running
-  example, we implement a type @{text "'a dlist"} of list consisting
+  example, we implement a type @{typ "'a dlist"} of lists consisting
   of distinct elements.
 
+  The specification of @{typ "'a dlist"} itself can be found in theory
+  @{theory Dlist}.
+
   The first step is to decide on which representation the abstract
-  type (in our example @{text "'a dlist"}) should be implemented.
-  Here we choose @{text "'a list"}.  Then a conversion from the concrete
+  type (in our example @{typ "'a dlist"}) should be implemented.
+  Here we choose @{typ "'a list"}.  Then a conversion from the concrete
   type to the abstract type must be specified, here:
 \<close>