# HG changeset patch
# User haftmann
# Date 1749066193 0
# Node ID e6f299c5dec6ef3f7fa95e87359f926e62fd50f6
# Parent  8575092e21fa49411c425cf788989eed16a4fa28
tuned syntax

diff -r 8575092e21fa -r e6f299c5dec6 src/HOL/List.thy
--- 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