# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1421843537 0
# Node ID c616ec6b1e3c3068e663d81a9d3b33c5dcf5a564
# Parent  652861c9473f59e3ac4f083edee609c335f29807
updated

diff -r 652861c9473f -r c616ec6b1e3c progs/scala/re.scala
--- a/progs/scala/re.scala	Mon Jan 19 09:55:58 2015 +0000
+++ b/progs/scala/re.scala	Wed Jan 21 12:32:17 2015 +0000
@@ -261,10 +261,17 @@
   result
 }
 
-val r = ("a" | "ab") ~ ("bcd" | "c")
-println(lexing(r, "abcd"))
-println(values(r).mkString("\n"))
-println(values(r).map(flatten).mkString("\n"))
+val r1 = ("a" | "ab") ~ ("bcd" | "c")
+println(lexing(r1, "abcd"))
+println(values(r1).mkString("\n"))
+println(values(r1).map(flatten).mkString("\n"))
+
+val r2 = ("" | "a") ~ ("ab" | "b")
+println(lexing(r2, "ab"))
+println(values(r2).mkString("\n"))
+println(values(r2).toList.map(flatten).mkString("\n"))
+
+
 
 // Two Simple Tests
 //===================
diff -r 652861c9473f -r c616ec6b1e3c thys/Re1.thy
--- a/thys/Re1.thy	Mon Jan 19 09:55:58 2015 +0000
+++ b/thys/Re1.thy	Wed Jan 21 12:32:17 2015 +0000
@@ -133,7 +133,7 @@
 using assms
 apply(induct)
 apply(auto)
-done
+oops
 
 
 section {* Posix definition *}
@@ -211,6 +211,7 @@
 apply(auto)
 apply (metis ValOrd.intros(1))
 apply (rule ValOrd.intros(2))
+oops
 
 lemma POSIX_ALT2:
   assumes "POSIX (Left v1) (ALT r1 r2)"
@@ -593,6 +594,7 @@
 apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
+apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(case_tac "c = c'")
@@ -600,8 +602,10 @@
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply (metis Prf.intros(5))
+apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
+apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply (metis Prf.intros(2))