# HG changeset patch
# User nipkow
# Date 1390489768 -3600
# Node ID 11408b65e9a6676339ed4ebe555e93ced84c9de9
# Parent  9f9db4e6fabc6fd1a8ef9cb94da686880418a39f
installed by Johannes in Extended now

diff -r 9f9db4e6fabc -r 11408b65e9a6 src/HOL/IMP/Abs_Int2_ivl.thy
--- 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"