src/Doc/Codegen/Adaptation.thy
changeset 51162 310b94ed1815
parent 51160 599ff65b85e2
child 51171 e8b2d90da499
     1.1 --- a/src/Doc/Codegen/Adaptation.thy	Fri Feb 15 11:47:34 2013 +0100
     1.2 +++ b/src/Doc/Codegen/Adaptation.thy	Fri Feb 15 12:48:20 2013 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4    \end{itemize}
     1.5  
     1.6    \noindent However, even if you ought refrain from setting up
     1.7 -  adaptation yourself, already the @{text "HOL"} comes with some
     1.8 +  adaptation yourself, already @{text "HOL"} comes with some
     1.9    reasonable default adaptations (say, using target language list
    1.10    syntax).  There also some common adaptation cases which you can
    1.11    setup by importing particular library theories.  In order to
    1.12 @@ -146,16 +146,10 @@
    1.13         by @{typ integer} and thus by target-language built-in integers;
    1.14         contains @{text "Code_Binary_Nat"} as a prerequisite.
    1.15  
    1.16 -    \item[@{text "Code_Target_Numeral"}] is a convenience node
    1.17 +    \item[@{text "Code_Target_Numeral"}] is a convenience theory
    1.18         containing both @{text "Code_Target_Nat"} and
    1.19         @{text "Code_Target_Int"}.
    1.20  
    1.21 -    \item[@{text "Efficient_Nat"}] \label{eff_nat} implements
    1.22 -       natural numbers by integers, which in general will result in
    1.23 -       higher efficiency; pattern matching with @{term "0\<Colon>nat"} /
    1.24 -       @{const "Suc"} is eliminated; includes @{text "Code_Integer"}
    1.25 -       and @{text "Code_Numeral"}.
    1.26 -
    1.27      \item[@{text "Code_Char"}] represents @{text HOL} characters by
    1.28         character literals in target languages.
    1.29  
    1.30 @@ -165,15 +159,11 @@
    1.31         for code setups which involve e.g.~printing (error) messages.
    1.32         Part of @{text "HOL-Main"}.
    1.33  
    1.34 -  \end{description}
    1.35 +    \item[@{theory "IArray"}] provides a type @{typ "'a iarray"}
    1.36 +       isomorphic to lists but implemented by (effectively immutable)
    1.37 +       arrays \emph{in SML only}.
    1.38  
    1.39 -  \begin{warn}
    1.40 -    When importing any of those theories which are not part of
    1.41 -    @{text "HOL-Main"}, they should form the last
    1.42 -    items in an import list.  Since these theories adapt the code
    1.43 -    generator setup in a non-conservative fashion, strange effects may
    1.44 -    occur otherwise.
    1.45 -  \end{warn}
    1.46 +  \end{description}
    1.47  *}
    1.48  
    1.49