diff -r 32b222d77fa0 -r 6746f5e1f1f8 thys/Lexer.thy
--- a/thys/Lexer.thy	Fri Aug 11 20:29:01 2017 +0100
+++ b/thys/Lexer.thy	Fri Aug 18 14:51:29 2017 +0100
@@ -38,7 +38,7 @@
 
 lemma mkeps_nullable:
   assumes "nullable(r)" 
-  shows "\<turnstile> mkeps r : r"
+  shows "\<Turnstile> mkeps r : r"
 using assms
 by (induct rule: nullable.induct) 
    (auto intro: Prf.intros)
@@ -49,22 +49,25 @@
 using assms
 by (induct rule: nullable.induct) (auto)
 
-lemma Prf_injval:
-  assumes "\<turnstile> v : der c r" 
-  shows "\<turnstile> (injval r c v) : r"
-using assms
-apply(induct r arbitrary: c v rule: rexp.induct)
-apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
-done
-
 lemma Prf_injval_flat:
-  assumes "\<turnstile> v : der c r" 
+  assumes "\<Turnstile> v : der c r" 
   shows "flat (injval r c v) = c # (flat v)"
 using assms
 apply(induct arbitrary: v rule: der.induct)
 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
 done
 
+lemma Prf_injval:
+  assumes "\<Turnstile> v : der c r" 
+  shows "\<Turnstile> (injval r c v) : r"
+using assms
+apply(induct r arbitrary: c v rule: rexp.induct)
+apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
+apply(simp add: Prf_injval_flat)
+done
+
+
+
 text {*
   Mkeps and injval produce, or preserve, Posix values.
 *}