dropped now obsolete hint;
authorhaftmann
Fri Feb 15 12:48:20 2013 +0100 (2013-02-15)
changeset 51162310b94ed1815
parent 51161 6ed12ae3b3e1
child 51163 4e53be4ad845
dropped now obsolete hint;
a few words on theory IArray;
dropped reference to obsolete theory Efficient_Nat
src/Doc/Codegen/Adaptation.thy
src/Doc/Codegen/Setup.thy
src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy
src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy
src/HOL/Codegenerator_Test/Generate_Target_Nat.thy
     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  
     2.1 --- a/src/Doc/Codegen/Setup.thy	Fri Feb 15 11:47:34 2013 +0100
     2.2 +++ b/src/Doc/Codegen/Setup.thy	Fri Feb 15 12:48:20 2013 +0100
     2.3 @@ -4,6 +4,7 @@
     2.4    "~~/src/HOL/Library/Dlist"
     2.5    "~~/src/HOL/Library/RBT"
     2.6    "~~/src/HOL/Library/Mapping"
     2.7 +  "~~/src/HOL/Library/IArray"
     2.8  begin
     2.9  
    2.10  (* FIXME avoid writing into source directory *)