doc-src/IsarRef/Thy/HOL_Specific.thy

     @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{attribute_def (HOL) code_unfold} & : & @{text attribute} \\
     @{attribute_def (HOL) code_post} & : & @{text attribute} \\
-    @{attribute_def (HOL) code_unfold_post} & : & @{text attribute} \\
+    @{attribute_def (HOL) code_abbrev} & : & @{text attribute} \\
     @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\

     ;
 
     @@{attribute (HOL) code_post} ( 'del' ) ?
     ;
 
-    @@{attribute (HOL) code_unfold_post}
+    @@{attribute (HOL) code_abbrev}
     ;
 
     @@{command (HOL) code_thms} ( constexpr + ) ?
     ;
 

 
   \item @{command (HOL) "print_codesetup"} gives an overview on
   selected code equations and code generator datatypes.
 
   \item @{attribute (HOL) code_unfold} declares (or with option
-  ``@{text "del"}'' removes) theorems which are applied as
-  rewrite rules to any code equation during preprocessing.
+  ``@{text "del"}'' removes) theorems which during preprocessing
+  are applied as rewrite rules to any code equation or evaluation
+  input.
 
   \item @{attribute (HOL) code_post} declares (or with option ``@{text
   "del"}'' removes) theorems which are applied as rewrite rules to any
   result of an evaluation.
 
-  \item @{attribute (HOL) code_unfold_post} declares equations which are
-  applied as rewrite rules to any code equation during preprocessing,
-  and symmetrically to any result of an evaluation.
-  
+  \item @{attribute (HOL) code_abbrev} declares equations which are
+  applied as rewrite rules to any result of an evaluation and
+  symmetrically during preprocessing to any code equation or evaluation
+  input.
+
   \item @{command (HOL) "print_codeproc"} prints the setup of the code
   generator preprocessor.
 
   \item @{command (HOL) "code_thms"} prints a list of theorems
   representing the corresponding program containing all given