# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1254474621 -7200
# Node ID 1585a60b076d56b5f7171f7a56917fc16c5eb596
# Parent  4826ad24f772e270465730338a075bca5b07e4e0# Parent  1a92820a5b85fd5988d2df5af81747dbad39f91b
Merged

diff -r 1a92820a5b85 -r 1585a60b076d QuotMain.thy
--- a/QuotMain.thy	Thu Oct 01 16:10:14 2009 +0200
+++ b/QuotMain.thy	Fri Oct 02 11:10:21 2009 +0200
@@ -703,6 +703,15 @@
   shows "(z # xs) \<approx> (z # ys)"
   using a by (rule QuotMain.list_eq.intros(5))
 
+lemma fs1_strong_cases:
+  fixes X :: "'a list"
+  shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
+  apply (induct X)
+  apply (simp)
+  apply (erule disjE)
+  apply (metis QuotMain.m1 list_eq_refl)
+  apply (metis QUOT_TYPE_I_fset.R_sym QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons)
+  done
 
 text {*
   Unlam_def converts a definition given as
@@ -1255,4 +1264,3 @@
 *)
 
 end
-