| changeset 68778 | 4566bac4517d |
| parent 67613 | ce654b0e6d69 |
| child 69505 | cc2d676d5395 |
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Mon Aug 20 20:54:40 2018 +0200 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy Tue Aug 21 17:29:46 2018 +0200 @@ -1,11 +1,11 @@ (* Author: Tobias Nipkow *) +subsection "Interval Analysis" + theory Abs_Int2_ivl imports Abs_Int2 begin -subsection "Interval Analysis" - type_synonym eint = "int extended" type_synonym eint2 = "eint * eint"