installed by Johannes in Extended now
authornipkow
Thu Jan 23 16:09:28 2014 +0100 (2014-01-23)
changeset 5512711408b65e9a6
parent 55126 9f9db4e6fabc
child 55128 6e16d2dd4f14
child 55130 70db8d380d62
installed by Johannes in Extended now
src/HOL/IMP/Abs_Int2_ivl.thy
     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