# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1423902921 0
# Node ID eb97e8361211a5dd363716f8641120f566d42c7d
# Parent  b31b224fa0e6c5e11865ef4e77dafd1f32ce3851
updated

diff -r b31b224fa0e6 -r eb97e8361211 progs/scala/re.scala
--- 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)
diff -r b31b224fa0e6 -r eb97e8361211 thys/Re1.thy
--- 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]
diff -r b31b224fa0e6 -r eb97e8361211 thys/notes.pdf
Binary file thys/notes.pdf has changed