installed by Johannes in Extended now

--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Thu Jan 23 16:02:02 2014 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Thu Jan 23 16:09:28 2014 +0100
@@ -6,10 +6,6 @@
 
 subsection "Interval Analysis"
 
-text{* Drop @{const Fin} around numerals on output from value command: *}
-declare Fin_numeral[code_post] Fin_neg_numeral[code_post]
-  zero_extended_def[symmetric, code_post] one_extended_def[symmetric, code_post]
-
 type_synonym eint = "int extended"
 type_synonym eint2 = "eint * eint"