diff -r a5427713eef4 -r 8c9349065477 thys/Re1.thy.rej
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Re1.thy.rej	Mon Oct 06 13:44:27 2014 +0100
@@ -0,0 +1,36 @@
+--- 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"