Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted a number of minor lemmas
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