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