# HG changeset patch
# User wenzelm
# Date 1330372530 -3600
# Node ID 9722171731af4430a8457dd88fd6bf04af477462
# Parent  61cd0ad6cd42f68fd07788f5d94222e9d4fb8c23
tuned proofs;

diff -r 61cd0ad6cd42 -r 9722171731af src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Mon Feb 27 20:42:09 2012 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Mon Feb 27 20:55:30 2012 +0100
@@ -217,10 +217,10 @@
   { 
     fix x 
     assume "length x = Suc 0"
-    hence "\<exists> l. x = [l]"  by - (cases x, auto)
+    hence "\<exists> l. x = [l]"  by (cases x) auto
   } note 0 = this
 
-  have "length a = Suc (Suc 0) \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
+  have "length a = Suc (Suc 0) \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a) (auto dest: 0)
   with * show ?thesis by (auto dest: 0)
 qed
 
diff -r 61cd0ad6cd42 -r 9722171731af src/HOL/MicroJava/DFA/LBVComplete.thy
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Mon Feb 27 20:42:09 2012 +0100
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Mon Feb 27 20:55:30 2012 +0100
@@ -169,7 +169,7 @@
 
 lemma (in lbv) top_le_conv [simp]:
   "\<top> <=_r x = (x = \<top>)"
-  by (insert semilat) (simp add: top top_le_conv) 
+  using semilat by (simp add: top) 
 
 lemma (in lbv) neq_top [simp, elim]:
   "\<lbrakk> x <=_r y; y \<noteq> \<top> \<rbrakk> \<Longrightarrow> x \<noteq> \<top>"