diff -r a2a7f65f538a -r 51444f205b5b thys/Re1.thy.rej
--- a/thys/Re1.thy.rej	Tue Oct 07 18:43:29 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
---- thys/Re1.thy	
-+++ thys/Re1.thy	
-@@ -168,6 +168,33 @@
- done
- *)
- 
-+
-+
-+
-+lemma POSIX_ALT2:
-+  assumes "POSIX (Left v1) (ALT r1 r2)"
-+  shows "POSIX v1 r1"
-+using assms
-+unfolding POSIX_def
-+apply(auto)
-+apply(drule_tac x="Left v'" in spec)
-+apply(simp)
-+apply(drule mp)
-+apply(rule Prf.intros)
-+apply(auto)
-+apply(erule ValOrd.cases)
-+apply(simp_all)
-+done
-+
-+lemma POSIX2_ALT:
-+  assumes "POSIX2 (Left v1) (ALT r1 r2)"
-+  shows "POSIX2 v1 r1"
-+using assms
-+unfolding POSIX2_def
-+apply(auto)
-+
-+done
-+
- lemma POSIX_ALT:
-   assumes "POSIX (Left v1) (ALT r1 r2)"
-   shows "POSIX v1 r1"