diff -r 11edadd16ebe -r 7b78e093f559 thys/Re1.thy
--- a/thys/Re1.thy	Thu Feb 26 12:43:59 2015 +0000
+++ b/thys/Re1.thy	Thu Feb 26 12:51:02 2015 +0000
@@ -42,7 +42,6 @@
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
-<<<<<<< local
 fun
  nullable :: "rexp \<Rightarrow> bool"
 where
@@ -51,19 +50,15 @@
 | "nullable (CHAR c) = False"
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
-=======
+
 value "L(CHAR c)"
 value "L(SEQ(CHAR c)(CHAR b))"
->>>>>>> other
 
-<<<<<<< local
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 apply (induct r) 
 apply(auto simp add: Sequ_def) 
 done
-=======
->>>>>>> other
 
 section {* Values *}
 
@@ -100,6 +95,7 @@
 | "flats(Right v) = flats(v)"
 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)"
 
+value "flats(Seq(Char c)(Char b))"
 
 section {* Relation between values and regular expressions *}
 
@@ -124,13 +120,8 @@
 apply(auto intro: Prf.intros)
 done
 
-<<<<<<< local
-=======
 value "flat(Seq(Char c)(Char b))"
 value "flat(Right(Void))"
->>>>>>> other
-
-<<<<<<< local
 
 lemma mkeps_flat:
   assumes "nullable(r)" shows "flat (mkeps r) = []"
@@ -143,17 +134,10 @@
   The value mkeps returns is always the correct POSIX
   value.
 *}
-=======
-fun flats :: "val \<Rightarrow> string list"
-where
-  "flats(Void) = [[]]"
-| "flats(Char c) = [[c]]"
-| "flats(Left v) = flats(v)"
-| "flats(Right v) = flats(v)"
-| "flats(Seq v1 v2) = (flats v1) @ (flats v2)"
->>>>>>> other
+
 
-value "flats(Seq(Char c)(Char b))"
+
+
 
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
@@ -175,7 +159,7 @@
 apply(auto)
 done
 
-definition definition prefix :: :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
+definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
 where
   "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"