# HG changeset patch
# User wenzelm
# Date 1736108256 -3600
# Node ID 94f018b2a4fb3866a822bbd80016dd66e9ee9b48
# Parent  60f21b6e4f572a421a64ce5c88d38e190b40a05f
tuned proofs;

diff -r 60f21b6e4f57 -r 94f018b2a4fb src/HOL/HOLCF/Library/List_Cpo.thy
--- a/src/HOL/HOLCF/Library/List_Cpo.thy	Sun Jan 05 18:10:34 2025 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Sun Jan 05 21:17:36 2025 +0100
@@ -16,21 +16,19 @@
 definition
   "xs \<sqsubseteq> ys \<longleftrightarrow> list_all2 (\<sqsubseteq>) xs ys"
 
-instance proof
-  fix xs :: "'a list"
-  from below_refl show "xs \<sqsubseteq> xs"
+instance
+proof
+  fix xs ys zs :: "'a list"
+  show "xs \<sqsubseteq> xs"
+    using below_refl 
     unfolding below_list_def
     by (rule list_all2_refl)
-next
-  fix xs ys zs :: "'a list"
-  assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> zs"
-  with below_trans show "xs \<sqsubseteq> zs"
+  show "xs \<sqsubseteq> ys \<Longrightarrow> ys \<sqsubseteq> zs \<Longrightarrow> xs \<sqsubseteq> zs"
+    using below_trans 
     unfolding below_list_def
     by (rule list_all2_trans)
-next
-  fix xs ys zs :: "'a list"
-  assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> xs"
-  with below_antisym show "xs = ys"
+  show "xs \<sqsubseteq> ys \<Longrightarrow> ys \<sqsubseteq> xs \<Longrightarrow> xs = ys"
+    using below_antisym
     unfolding below_list_def
     by (rule list_all2_antisym)
 qed