diff -r c892847df987 -r 0c666a0c57d7 thys2/Positions.thy
--- a/thys2/Positions.thy	Tue Dec 14 16:32:33 2021 +0000
+++ b/thys2/Positions.thy	Fri Jan 07 22:25:26 2022 +0000
@@ -206,37 +206,34 @@
   shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
 unfolding ordering_def PosOrd_ex_eq_def
 apply(auto)
-using PosOrd_irrefl apply blast
-using PosOrd_assym apply blast
-using PosOrd_trans by blast
+using PosOrd_trans partial_preordering_def apply blast
+using PosOrd_assym ordering_axioms_def by blast
 
 lemma PosOrd_order:
   shows "class.order (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
 using PosOrd_ordering
 apply(simp add: class.order_def class.preorder_def class.order_axioms_def)
-unfolding ordering_def
-by blast
+  by (metis (full_types) PosOrd_ex_eq_def PosOrd_irrefl PosOrd_trans)
 
 
 lemma PosOrd_ex_eq2:
   shows "v1 :\<sqsubset>val v2 \<longleftrightarrow> (v1 :\<sqsubseteq>val v2 \<and> v1 \<noteq> v2)"
-using PosOrd_ordering 
-unfolding ordering_def
-by auto
+  using PosOrd_ordering
+  using PosOrd_ex_eq_def PosOrd_irrefl by blast 
 
 lemma PosOrdeq_trans:
   assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v3"
   shows "v1 :\<sqsubseteq>val v3"
 using assms PosOrd_ordering 
-unfolding ordering_def
-by blast
+  unfolding ordering_def
+  by (metis partial_preordering.trans)
 
 lemma PosOrdeq_antisym:
   assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v1"
   shows "v1 = v2"
 using assms PosOrd_ordering 
-unfolding ordering_def
-by blast
+  unfolding ordering_def
+  by (simp add: ordering_axioms_def)
 
 lemma PosOrdeq_refl:
   shows "v :\<sqsubseteq>val v"