# 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 |\| A |\| B" by (rule Un_upper1[Transfer.transferred]) -lemma funion_upper2P: "B |\| A |\| B" +lemma funion_upper2: "B |\| A |\| B" by (rule Un_upper2[Transfer.transferred]) lemma funion_least: "A |\| C \ B |\| C \ A |\| B |\| C"