--- a/src/HOL/IMP/Abs_State.thy Mon Aug 20 20:54:40 2018 +0200 +++ b/src/HOL/IMP/Abs_State.thy Tue Aug 21 17:29:46 2018 +0200 @@ -1,5 +1,7 @@ (* Author: Tobias Nipkow *) +subsection "Computable State" + theory Abs_State imports Abs_Int0 begin