# HG changeset patch
# User desharna
# Date 1684273280 -7200
# Node ID 8122e865687eba9cd54088c931ed277583ced675
# Parent  0252d635bfb2eb3c63cb836412de168644a93e1d
fixed lemma name

diff -r 0252d635bfb2 -r 8122e865687e src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Tue May 16 22:23:05 2023 +0200
+++ b/src/HOL/Library/FSet.thy	Tue May 16 23:41:20 2023 +0200
@@ -559,7 +559,7 @@
 lemma funion_upper1: "A |\<subseteq>| A |\<union>| B"
   by (rule Un_upper1[Transfer.transferred])
 
-lemma funion_upper2P: "B |\<subseteq>| A |\<union>| B"
+lemma funion_upper2: "B |\<subseteq>| A |\<union>| B"
   by (rule Un_upper2[Transfer.transferred])
 
 lemma funion_least: "A |\<subseteq>| C \<Longrightarrow> B |\<subseteq>| C \<Longrightarrow> A |\<union>| B |\<subseteq>| C"