src/HOL/Analysis/Abstract_Limits.thy
6 weeks ago paulson 2019-03-07 renamed the constant "limit" as it is too "generic"
6 weeks ago paulson 2019-03-07 new material for Analysis