--- 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
--- 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>"