theory Abs_Int_init imports "HOL-Library.While_Combinator" "HOL-Library.Extended" Vars Collecting Abs_Int_Tests begin hide_const (open) top bot dom --"to avoid qualified names" end