--- a/thys/Spec.thy	Fri Aug 17 12:00:25 2018 +0100
+++ b/thys/Spec.thy	Sat Aug 18 01:54:44 2018 +0100
@@ -395,7 +395,7 @@
   moreover 
   have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" 
   unfolding S1_def S2_def f_def
-  unfolding LV_def image_def prefix_def strict_suffix_def
+  unfolding LV_def image_def prefix_def strict_suffix_def 
   apply(auto)
   apply(case_tac x)
   apply(auto elim: Prf_elims)
@@ -559,16 +559,21 @@
 
 
 text {*
-  Our POSIX value is a lexical value.
+  Our POSIX values are lexical values.
 *}
 
 lemma Posix_LV:
   assumes "s \<in> r \<rightarrow> v"
   shows "v \<in> LV r s"
-using assms unfolding LV_def
-apply(induct rule: Posix.induct)
-apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)
-done
+  using assms unfolding LV_def
+  apply(induct rule: Posix.induct)
+  apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)
+  done
 
+lemma Posix_Prf:
+  assumes "s \<in> r \<rightarrow> v"
+  shows "\<Turnstile> v : r"
+  using assms Posix_LV LV_def
+  by simp
 
 end
\ No newline at end of file