# HG changeset patch
# User wenzelm
# Date 1713446424 -7200
# Node ID bc450c8754ef7b5f5df292dcca5f563f2f9c998d
# Parent  e414bcc5a39ea6d196e3ac41e25e492e146c05e2# Parent  e07f29df1c676966261b7e360a92b622b08981aa
merged

diff -r e07f29df1c67 -r bc450c8754ef CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Apr 18 11:39:51 2024 +0200
+++ b/CONTRIBUTORS	Thu Apr 18 15:20:24 2024 +0200
@@ -14,6 +14,9 @@
 * March 2024: Manuel Eberl
   Weierstraß Factorization Theorem in HOL-Complex_Analysis.
 
+* March 2024: Ata Keskin
+  Analysis lemmas drawn from the Martingales AFP entry.
+
 * March 2024: Anthony Bordg, Manuel Eberl, Wenda Li, Larry Paulson
   New and more general definition of meromorphicity in HOL-Complex_Analysis.
 
diff -r e07f29df1c67 -r bc450c8754ef src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Thu Apr 18 11:39:51 2024 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Thu Apr 18 15:20:24 2024 +0200
@@ -2,6 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
     Author:     Robert Himmelmann, TU Muenchen
     Author:     Brian Huffman, Portland State University
+    Author:     Ata Keskin, TU Muenchen
 *)
 
 chapter \<open>Elementary Metric Spaces\<close>
diff -r e07f29df1c67 -r bc450c8754ef src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Thu Apr 18 11:39:51 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Thu Apr 18 15:20:24 2024 +0200
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Analysis/Set_Integral.thy
     Author:     Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
     Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
+    Author:     Ata Keskin, TU Muenchen
 
 Notation and useful facts for working with integrals over a set.