src/HOL/IMP/Abs_Int2_ivl.thy
changeset 55127 11408b65e9a6
parent 55125 0e0c09fca7bc
child 55565 f663fc1e653b
     1.1 --- a/src/HOL/IMP/Abs_Int2_ivl.thy	Thu Jan 23 16:02:02 2014 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Thu Jan 23 16:09:28 2014 +0100
     1.3 @@ -6,10 +6,6 @@
     1.4  
     1.5  subsection "Interval Analysis"
     1.6  
     1.7 -text{* Drop @{const Fin} around numerals on output from value command: *}
     1.8 -declare Fin_numeral[code_post] Fin_neg_numeral[code_post]
     1.9 -  zero_extended_def[symmetric, code_post] one_extended_def[symmetric, code_post]
    1.10 -
    1.11  type_synonym eint = "int extended"
    1.12  type_synonym eint2 = "eint * eint"
    1.13