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.
tuned syntax
authorhaftmann
Wed, 04 Jun 2025 19:43:13 +0000
changeset 82686 e6f299c5dec6
parent 82685 8575092e21fa
child 82687 97b9ac57751e
tuned syntax
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/List.thy	Wed Jun 04 09:52:40 2025 +0200
+++ b/src/HOL/List.thy	Wed Jun 04 19:43:13 2025 +0000
@@ -8279,8 +8279,8 @@
   by simp
 
 lemma subset_code [code]:
-  "set xs \<le> B \<longleftrightarrow> (\<forall>x\<in>set xs. x \<in> B)"
-  "A \<le> List.coset ys \<longleftrightarrow> (\<forall>y\<in>set ys. y \<notin> A)"
+  "set xs \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>set xs. x \<in> B)"
+  "A \<subseteq> List.coset ys \<longleftrightarrow> (\<forall>y\<in>set ys. y \<notin> A)"
   "List.coset [] \<subseteq> set [] \<longleftrightarrow> False"
   by auto
isabelle