# HG changeset patch
# User haftmann
# Date 1360928900 -3600
# Node ID 310b94ed1815f42c728c5cae2742b355fbb41dd1
# Parent  6ed12ae3b3e119a391dced22105f0bd5cc5be875
dropped now obsolete hint;
a few words on theory IArray;
dropped reference to obsolete theory Efficient_Nat

diff -r 6ed12ae3b3e1 -r 310b94ed1815 src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Fri Feb 15 11:47:34 2013 +0100
+++ b/src/Doc/Codegen/Adaptation.thy	Fri Feb 15 12:48:20 2013 +0100
@@ -55,7 +55,7 @@
   \end{itemize}
 
   \noindent However, even if you ought refrain from setting up
-  adaptation yourself, already the @{text "HOL"} comes with some
+  adaptation yourself, already @{text "HOL"} comes with some
   reasonable default adaptations (say, using target language list
   syntax).  There also some common adaptation cases which you can
   setup by importing particular library theories.  In order to
@@ -146,16 +146,10 @@
        by @{typ integer} and thus by target-language built-in integers;
        contains @{text "Code_Binary_Nat"} as a prerequisite.
 
-    \item[@{text "Code_Target_Numeral"}] is a convenience node
+    \item[@{text "Code_Target_Numeral"}] is a convenience theory
        containing both @{text "Code_Target_Nat"} and
        @{text "Code_Target_Int"}.
 
-    \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 @{text "Code_Integer"}
-       and @{text "Code_Numeral"}.
-
     \item[@{text "Code_Char"}] represents @{text HOL} characters by
        character literals in target languages.
 
@@ -165,15 +159,11 @@
        for code setups which involve e.g.~printing (error) messages.
        Part of @{text "HOL-Main"}.
 
-  \end{description}
+    \item[@{theory "IArray"}] provides a type @{typ "'a iarray"}
+       isomorphic to lists but implemented by (effectively immutable)
+       arrays \emph{in SML only}.
 
-  \begin{warn}
-    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.
-  \end{warn}
+  \end{description}
 *}
 
 
diff -r 6ed12ae3b3e1 -r 310b94ed1815 src/Doc/Codegen/Setup.thy
--- a/src/Doc/Codegen/Setup.thy	Fri Feb 15 11:47:34 2013 +0100
+++ b/src/Doc/Codegen/Setup.thy	Fri Feb 15 12:48:20 2013 +0100
@@ -4,6 +4,7 @@
   "~~/src/HOL/Library/Dlist"
   "~~/src/HOL/Library/RBT"
   "~~/src/HOL/Library/Mapping"
+  "~~/src/HOL/Library/IArray"
 begin
 
 (* FIXME avoid writing into source directory *)