diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Abs_Int1_const.thy --- a/src/HOL/IMP/Abs_Int1_const.thy Mon Aug 20 20:54:40 2018 +0200 +++ b/src/HOL/IMP/Abs_Int1_const.thy Tue Aug 21 17:29:46 2018 +0200 @@ -1,11 +1,11 @@ (* Author: Tobias Nipkow *) +subsection "Constant Propagation" + theory Abs_Int1_const imports Abs_Int1 begin -subsection "Constant Propagation" - datatype const = Const val | Any fun \_const where