Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed lemma name
authordesharna
Tue, 16 May 2023 23:41:20 +0200
changeset 78104 8122e865687e
parent 78103 0252d635bfb2
child 78105 ab8310c0e6d9
fixed lemma name
src/HOL/Library/FSet.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle