--- a/thys/Spec.thy	Fri Aug 25 23:54:10 2017 +0200
+++ b/thys/Spec.thy	Sun Aug 27 00:03:31 2017 +0300
@@ -543,34 +543,15 @@
 
 
 text {*
-  Our POSIX value is a canonical value.
+  Our POSIX value is a lexical value.
 *}
 
 lemma Posix_LV:
   assumes "s \<in> r \<rightarrow> v"
   shows "v \<in> LV r s"
-using assms
+using assms unfolding LV_def
 apply(induct rule: Posix.induct)
-apply(auto simp add: LV_def intro: Prf.intros elim: Prf.cases)
-apply(rotate_tac 5)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rule Prf.intros)
-apply(simp_all)
+apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)
 done
 
-(*
-lemma test2: 
-  assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
-  shows "(Stars vs) \<in> LV (STAR r) (flat (Stars vs))" 
-using assms
-apply(induct vs)
-apply(auto simp add: LV_def)
-apply(rule Prf.intros)
-apply(simp)
-apply(rule Prf.intros)
-apply(simp_all)
-by (metis (no_types, lifting) LV_def Posix_LV mem_Collect_eq)
-*)
-
 end
\ No newline at end of file