--- a/progs/scala/re.scala	Thu Feb 12 14:00:45 2015 +0000
+++ b/progs/scala/re.scala	Sat Feb 14 08:35:21 2015 +0000
@@ -296,6 +296,17 @@
 //Some experiments
 //================
 
+val f0 = ("ab" | "b" | "cb")
+val f1 = der('a', f0)
+val f2 = der('b', f1)
+val g2 = mkeps(f2)
+val g1 = inj(f1, 'b', g2)
+val g0 = inj(f0, 'a', g1)
+
+lex((("" | "a") ~ ("ab" | "b")), "ab".toList)
+lex((("" | "a") ~ ("b" | "ab")), "ab".toList)
+lex((("" | "a") ~ ("c" | "ab")), "ab".toList)
+
 val reg0 = ("" | "a") ~ ("ab" | "b")
 val reg1 = der('a', reg0)
 val reg2 = der('b', reg1)

--- a/thys/Re1.thy	Thu Feb 12 14:00:45 2015 +0000
+++ b/thys/Re1.thy	Sat Feb 14 08:35:21 2015 +0000
@@ -321,7 +321,7 @@
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply (metis ValOrd.intros)
-apply(simp add: POSIX_def)
+apply(simp)
 apply(auto)[1]
 apply(simp add: POSIX_def)
 apply(auto)[1]

Binary file thys/notes.pdf has changed