diff -r 25b7d6bfd294 -r d688a01b8f89 thys/Positions.thy
--- a/thys/Positions.thy	Tue Aug 21 14:14:19 2018 +0100
+++ b/thys/Positions.thy	Mon Sep 10 21:41:54 2018 +0100
@@ -726,8 +726,12 @@
 using Least_existence[OF assms] assms
 using PosOrdeq_antisym by blast
 
-
-
+lemma Least_existence2:
+  assumes "LV r s \<noteq> {}"
+  shows " \<exists>!vmin \<in> LV r s. lexer r s = Some vmin \<and> (\<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v)"
+using Least_existence[OF assms] assms
+using PosOrdeq_antisym 
+  using PosOrd_Posix PosOrd_ex_eq2 lexer_correctness(1) by auto
 
 
 lemma Least_existence1_pre: