| changeset 81182 | fc5066122e68 |
| parent 80934 | 8e72f55295fd |
| child 82338 | 1eb12389c499 |
--- a/src/HOL/Filter.thy Fri Oct 18 11:44:05 2024 +0200 +++ b/src/HOL/Filter.thy Fri Oct 18 14:20:09 2024 +0200 @@ -1308,10 +1308,8 @@ syntax "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder LIM\<close>\<close>LIM (_)/ (_)./ (_) :> (_))\<close> [1000, 10, 0, 10] 10) - syntax_consts "_LIM" == filterlim - translations "LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"