# HG changeset patch
# User haftmann
# Date 1361126340 -3600
# Node ID e8b2d90da4998129c4891506d8d63e979a722174
# Parent  b3cdcba073d58141490cf1f14178f81992092dcd
corrected and clarified Code_Binary_Nat vs. Code_Target_Nat

diff -r b3cdcba073d5 -r e8b2d90da499 src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Sun Feb 17 11:34:40 2013 +0100
+++ b/src/Doc/Codegen/Adaptation.thy	Sun Feb 17 19:39:00 2013 +0100
@@ -136,15 +136,16 @@
     \item[@{text "Code_Target_Int"}] implements type @{typ int}
        by @{typ integer} and thus by target-language built-in integers.
 
-    \item[@{text "Code_Binary_Nat"}] \label{eff_nat} implements type
+    \item[@{text "Code_Binary_Nat"}] implements type
        @{typ nat} using a binary rather than a linear representation,
        which yields a considerable speedup for computations.
        Pattern matching with @{term "0\<Colon>nat"} / @{const "Suc"} is eliminated
-       by a preprocessor.
+       by a preprocessor.\label{abstract_nat}
 
-    \item[@{text "Code_Target_Nat"}] implements type @{typ int}
-       by @{typ integer} and thus by target-language built-in integers;
-       contains @{text "Code_Binary_Nat"} as a prerequisite.
+    \item[@{text "Code_Target_Nat"}] implements type @{typ nat}
+       by @{typ integer} and thus by target-language built-in integers.
+       Pattern matching with @{term "0\<Colon>nat"} / @{const "Suc"} is eliminated
+       by a preprocessor.
 
     \item[@{text "Code_Target_Numeral"}] is a convenience theory
        containing both @{text "Code_Target_Nat"} and
diff -r b3cdcba073d5 -r e8b2d90da499 src/Doc/Codegen/Foundations.thy
--- a/src/Doc/Codegen/Foundations.thy	Sun Feb 17 11:34:40 2013 +0100
+++ b/src/Doc/Codegen/Foundations.thy	Sun Feb 17 19:39:00 2013 +0100
@@ -117,8 +117,8 @@
   interface, transforming a list of function theorems to another list
   of function theorems, provided that neither the heading constant nor
   its type change.  The @{term "0\<Colon>nat"} / @{const Suc} pattern
-  elimination implemented in theory @{text Code_Binary_Nat} (see
-  \secref{eff_nat}) uses this interface.
+  used in theory @{text Code_Abstract_Nat} (see \secref{abstract_nat})
+  uses this interface.
 
   \noindent The current setup of the preprocessor may be inspected
   using the @{command_def print_codeproc} command.  @{command_def