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