equal
deleted
inserted
replaced
1031 proof |
1031 proof |
1032 assume h: "?D = {}" |
1032 assume h: "?D = {}" |
1033 show ?thesis by (unfold h, simp) |
1033 show ?thesis by (unfold h, simp) |
1034 next |
1034 next |
1035 assume "\<exists> a. ?D = {a}" |
1035 assume "\<exists> a. ?D = {a}" |
1036 thus ?thesis by auto |
1036 thus ?thesis |
|
1037 by (metis finite.simps) |
1037 qed |
1038 qed |
1038 qed |
1039 qed |
1039 ultimately show ?thesis by simp |
1040 ultimately show ?thesis by simp |
1040 next |
1041 next |
1041 case (P th cs) |
1042 case (P th cs) |