--- a/src/HOL/Real_Asymp/Real_Asymp_Examples.thy Fri Oct 17 15:42:50 2025 +0100
+++ b/src/HOL/Real_Asymp/Real_Asymp_Examples.thy Sat Oct 18 13:14:55 2025 +0100
@@ -11,6 +11,13 @@
lemma "((\<lambda>x::real. exp x * (exp (1/x - exp (-x)) - exp (1/x))) \<longlongrightarrow> -1) at_top"
by real_asymp
+
+text \<open>Also works with schematic goals!\<close>
+lemma "\<exists>L. ((\<lambda>x::real. exp x * (exp (1/x - exp (-x)) - exp (1/x))) \<longlongrightarrow> L) at_top \<and> L<0"
+ apply (intro exI conjI)
+ apply real_asymp
+ apply auto
+ done
lemma "((\<lambda>x::real. exp x * (exp (1/x + exp (-x) + exp (-(x^2))) -
exp (1/x - exp (-exp x)))) \<longlongrightarrow> 1) at_top"