--- a/thys/Positions.thy	Fri Aug 25 15:05:20 2017 +0200
+++ b/thys/Positions.thy	Fri Aug 25 23:52:49 2017 +0200
@@ -671,6 +671,7 @@
     by (auto simp add: LV_def)
   then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast         
   then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
+    thm PosOrd_SeqI1 PosOrd_SeqI2
     unfolding  PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) 
   then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
 next 
@@ -690,11 +691,10 @@
   unfolding LV_def  
   apply(auto)
   apply(erule Prf.cases)
-  apply(simp_all)
-  apply(auto)[1]
+  apply(auto)
   apply(case_tac vs)
-  apply(auto)
-  using Prf.intros(6) by blast
+  apply(auto intro: Prf.intros)
+  done
   then show "Stars (v # vs) :\<sqsubseteq>val v3" 
     proof (cases)
       case (NonEmpty v3a vs3)
@@ -821,8 +821,10 @@
 next 
   case (ONE s v1)
   have "v1 \<in> LV ONE s" by fact
-  then show "s \<in> ONE \<rightarrow> v1" unfolding LV_def
-    by(auto elim!: Prf.cases intro: Posix.intros)
+  then have "v1 = Void" "s = []" unfolding LV_def
+    by(auto elim: Prf.cases)
+  then show "s \<in> ONE \<rightarrow> v1" 
+    by(auto intro: Posix.intros)
 next 
   case (CHAR c s v1)
   have "v1 \<in> LV (CHAR c) s" by fact
@@ -832,7 +834,7 @@
   case (ALT r1 r2 s v1)
   have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
   have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
-  have as1: "\<forall>v2\<in>LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
+  have as1: "\<forall>v2 \<in> LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
   have as2: "v1 \<in> LV (ALT r1 r2) s" by fact
   then consider 
      (Left) v1' where
@@ -845,18 +847,17 @@
   then show "s \<in> ALT r1 r2 \<rightarrow> v1"
    proof (cases)
      case (Left v1')
-     have "v1' \<in> LV r1 s" using as2
-       unfolding LV_def Left by (auto elim: Prf.cases)
+     have "v1' \<in> LV r1 s" using Left(3) .
      moreover
      have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
-       unfolding LV_def Left using Prf.intros(2) PosOrd_Left_eq by force  
+       unfolding Left(1,2) unfolding LV_def 
+       using Prf.intros(2) PosOrd_Left_eq by force  
      ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
      then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros)
      then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
    next
      case (Right v1')
-     have "v1' \<in> LV r2 s" using as2
-       unfolding LV_def Right by (auto elim: Prf.cases)
+     have "v1' \<in> LV r2 s" using Right(3) .
      moreover
      have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1
        unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force