src/HOL/Bali/Decl.thy

--- a/src/HOL/Bali/Decl.thy	Fri Nov 15 21:43:22 2024 +0100
+++ b/src/HOL/Bali/Decl.thy	Fri Nov 15 23:20:24 2024 +0100
@@ -68,24 +68,20 @@
 instance
 proof
   fix x y z::acc_modi
-  show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
+  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
     by (auto simp add: le_acc_def less_acc_def split: acc_modi.split) 
   show "x \<le> x"                       \<comment> \<open>reflexivity\<close>
     by (auto simp add: le_acc_def)
-  {
-    assume "x \<le> y" "y \<le> z"           \<comment> \<open>transitivity\<close> 
-    then show "x \<le> z"
-      by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
-  next
-    assume "x \<le> y" "y \<le> x"           \<comment> \<open>antisymmetry\<close>
-    moreover have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
+  show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"  \<comment> \<open>transitivity\<close>
+    by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
+  show "x = y" if "x \<le> y" "y \<le> x"   \<comment> \<open>antisymmetry\<close>
+  proof -
+    have "\<forall>x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
       by (auto simp add: less_acc_def split: acc_modi.split)
-    ultimately show "x = y" by (unfold le_acc_def) iprover
-  next
-    fix x y:: acc_modi
-    show "x \<le> y \<or> y \<le> x"   
-      by (auto simp add: less_acc_def le_acc_def split: acc_modi.split)
-  }
+    with that show ?thesis by (unfold le_acc_def) iprover
+  qed
+  show "x \<le> y \<or> y \<le> x"
+    by (auto simp add: less_acc_def le_acc_def split: acc_modi.split)
 qed
   
 end