src/Doc/Codegen/Adaptation.thy
changeset 51171 e8b2d90da499
parent 51162 310b94ed1815
child 51172 16eb76ca1e4a
     1.1 --- a/src/Doc/Codegen/Adaptation.thy	Sun Feb 17 11:34:40 2013 +0100
     1.2 +++ b/src/Doc/Codegen/Adaptation.thy	Sun Feb 17 19:39:00 2013 +0100
     1.3 @@ -136,15 +136,16 @@
     1.4      \item[@{text "Code_Target_Int"}] implements type @{typ int}
     1.5         by @{typ integer} and thus by target-language built-in integers.
     1.6  
     1.7 -    \item[@{text "Code_Binary_Nat"}] \label{eff_nat} implements type
     1.8 +    \item[@{text "Code_Binary_Nat"}] implements type
     1.9         @{typ nat} using a binary rather than a linear representation,
    1.10         which yields a considerable speedup for computations.
    1.11         Pattern matching with @{term "0\<Colon>nat"} / @{const "Suc"} is eliminated
    1.12 -       by a preprocessor.
    1.13 +       by a preprocessor.\label{abstract_nat}
    1.14  
    1.15 -    \item[@{text "Code_Target_Nat"}] implements type @{typ int}
    1.16 -       by @{typ integer} and thus by target-language built-in integers;
    1.17 -       contains @{text "Code_Binary_Nat"} as a prerequisite.
    1.18 +    \item[@{text "Code_Target_Nat"}] implements type @{typ nat}
    1.19 +       by @{typ integer} and thus by target-language built-in integers.
    1.20 +       Pattern matching with @{term "0\<Colon>nat"} / @{const "Suc"} is eliminated
    1.21 +       by a preprocessor.
    1.22  
    1.23      \item[@{text "Code_Target_Numeral"}] is a convenience theory
    1.24         containing both @{text "Code_Target_Nat"} and