# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1536612114 -3600
# Node ID d688a01b8f890cfecc4c42a4bbbedfea86786a08
# Parent  25b7d6bfd294fd9284d8a7f9336b997e6c40974f
updated

diff -r 25b7d6bfd294 -r d688a01b8f89 thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Tue Aug 21 14:14:19 2018 +0100
+++ b/thys/Journal/Paper.thy	Mon Sep 10 21:41:54 2018 +0100
@@ -1355,7 +1355,7 @@
   regular expression @{text r} and string @{term s} is in fact a
   minimal element of the values in @{text "LV r s"}. By
   Proposition~\ref{ordlen}\textit{(2)} we also know that any value in
-  @{text "LV s' r"}, with @{term "s'"} being a strict prefix, cannot be
+  @{text "LV r s'"}, with @{term "s'"} being a strict prefix, cannot be
   smaller than @{text "v\<^sub>1"}. The next theorem shows the
   opposite---namely any minimal element in @{term "LV r s"} must be a
   @{text POSIX} value. This can be established by induction on @{text
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: