# HG changeset patch
# User wenzelm
# Date 1294844017 -3600
# Node ID a42cbf5b44c82fe5941a6c92b6cacf3c0daa9d5e
# Parent  4d2f9a1c24c705d4993364e9be093946c3e5aaa3
tuned proof;

diff -r 4d2f9a1c24c7 -r a42cbf5b44c8 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Wed Jan 12 15:38:57 2011 +0100
+++ b/src/HOL/Bali/Decl.thy	Wed Jan 12 15:53:37 2011 +0100
@@ -64,30 +64,26 @@
 definition
   le_acc_def: "(a :: acc_modi) \<le> b \<longleftrightarrow> a < b \<or> a = b"
 
-instance proof
+instance
+proof
   fix x y z::acc_modi
   show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
     by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 
-  {
   show "x \<le> x"               \<spacespace>\<spacespace>    -- reflexivity
     by (auto simp add: le_acc_def)
-  next
-  assume "x \<le> y" "y \<le> z"           -- transitivity 
-  thus "x \<le> z"
-    by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
+  {
+    assume "x \<le> y" "y \<le> z"           -- transitivity 
+    then show "x \<le> z"
+      by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
   next
-  assume "x \<le> y" "y \<le> x"           -- antisymmetry
-  thus "x = y"
-  proof -
-    have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
+    assume "x \<le> y" "y \<le> x"           -- antisymmetry
+    moreover have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
       by (auto simp add: less_acc_def split add: acc_modi.split)
-    with prems show ?thesis
-      by (unfold le_acc_def) iprover
-  qed
+    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 add: acc_modi.split)
+    fix x y:: acc_modi
+    show "x \<le> y \<or> y \<le> x"   
+      by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
   }
 qed