# HG changeset patch
# User haftmann
# Date 1749717477 -7200
# Node ID 81f64077eaabfcbed85bc3265523bd85c9678dd2
# Parent  8f0b2daa7eaab6beda448da39a48271b5d49535b
tuned whitespace

diff -r 8f0b2daa7eaa -r 81f64077eaab src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/List.thy	Thu Jun 12 10:37:57 2025 +0200
@@ -7945,7 +7945,7 @@
 text \<open>Executable checks for relations on sets\<close>
 
 definition listrel1p :: \<open>('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close> \<comment> \<open>only for code generation\<close>
-  where  \<open>listrel1p r xs ys \<longleftrightarrow> (xs, ys) \<in> listrel1 {(x, y). r x y}\<close>
+  where \<open>listrel1p r xs ys \<longleftrightarrow> (xs, ys) \<in> listrel1 {(x, y). r x y}\<close>
 
 lemma [code_unfold]:
   \<open>(xs, ys) \<in> listrel1 r \<longleftrightarrow> listrel1p (\<lambda>x y. (x, y) \<in> r) xs ys\<close>