--- a/thys/Re1.thy	Thu Jan 29 09:05:40 2015 +0000
+++ b/thys/Re1.thy	Thu Jan 29 11:23:05 2015 +0000
@@ -42,6 +42,9 @@
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
+value "L(CHAR c)"
+value "L(SEQ(CHAR c)(CHAR b))"
+
 
 section {* Values *}
 
@@ -72,6 +75,9 @@
 | "flat(Right v) = flat(v)"
 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
 
+value "flat(Seq(Char c)(Char b))"
+value "flat(Right(Void))"
+
 fun flats :: "val \<Rightarrow> string list"
 where
   "flats(Void) = [[]]"
@@ -80,6 +86,8 @@
 | "flats(Right v) = flats(v)"
 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)"
 
+value "flats(Seq(Char c)(Char b))"
+
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
@@ -100,7 +108,7 @@
 apply(auto)
 done
 
-definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
+definition definition prefix :: :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
 where
   "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"