# HG changeset patch
# User haftmann
# Date 1329592318 -3600
# Node ID 17dde5feea4bda3ca6dbfbea20b2f227408d196e
# Parent  11b6471c2f50c46cf07fce27e0703df0404a0a5b
clarified

diff -r 11b6471c2f50 -r 17dde5feea4b doc-src/Codegen/Thy/Adaptation.thy
--- a/doc-src/Codegen/Thy/Adaptation.thy	Sat Feb 18 20:07:47 2012 +0100
+++ b/doc-src/Codegen/Thy/Adaptation.thy	Sat Feb 18 20:11:58 2012 +0100
@@ -125,36 +125,38 @@
 
   \begin{description}
 
-    \item[@{theory "Code_Integer"}] represents @{text HOL} integers by
+    \item[@{text "Code_Integer"}] represents @{text HOL} integers by
        big integer literals in target languages.
 
-    \item[@{theory "Code_Char"}] represents @{text HOL} characters by
+    \item[@{text "Code_Char"}] represents @{text HOL} characters by
        character literals in target languages.
 
-    \item[@{theory "Code_Char_chr"}] like @{text "Code_Char"}, but
-       also offers treatment of character codes; includes @{theory
+    \item[@{text "Code_Char_chr"}] like @{text "Code_Char"}, but
+       also offers treatment of character codes; includes @{text
        "Code_Char"}.
 
-    \item[@{theory "Efficient_Nat"}] \label{eff_nat} implements
+    \item[@{text "Efficient_Nat"}] \label{eff_nat} implements
        natural numbers by integers, which in general will result in
        higher efficiency; pattern matching with @{term "0\<Colon>nat"} /
-       @{const "Suc"} is eliminated; includes @{theory "Code_Integer"}
-       and @{theory "Code_Numeral"}.
+       @{const "Suc"} is eliminated; includes @{text "Code_Integer"}
+       and @{text "Code_Numeral"}.
 
     \item[@{theory "Code_Numeral"}] provides an additional datatype
        @{typ index} which is mapped to target-language built-in
        integers.  Useful for code setups which involve e.g.~indexing
-       of target-language arrays.
+       of target-language arrays.  Part of @{text "HOL-Main"}.
 
     \item[@{theory "String"}] provides an additional datatype @{typ
        String.literal} which is isomorphic to strings; @{typ
        String.literal}s are mapped to target-language strings.  Useful
        for code setups which involve e.g.~printing (error) messages.
+       Part of @{text "HOL-Main"}.
 
   \end{description}
 
   \begin{warn}
-    When importing any of these theories, they should form the last
+    When importing any of those theories which are not part of
+    @{text "HOL-Main"}, they should form the last
     items in an import list.  Since these theories adapt the code
     generator setup in a non-conservative fashion, strange effects may
     occur otherwise.
@@ -342,3 +344,4 @@
 *}
 
 end
+