--- a/src/HOL/Bali/TypeRel.thy Wed Mar 28 11:46:14 2012 +0200
+++ b/src/HOL/Bali/TypeRel.thy Wed Mar 28 12:08:08 2012 +0200
@@ -200,9 +200,10 @@
qed
qed
-lemma subclseq_cases [consumes 1, case_names Eq Subcls]:
- "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; C = D \<Longrightarrow> P; G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by (blast intro: rtrancl_cases)
+lemma subclseq_cases:
+ assumes "G\<turnstile>C \<preceq>\<^sub>C D"
+ obtains (Eq) "C = D" | (Subcls) "G\<turnstile>C \<prec>\<^sub>C D"
+using assms by (blast intro: rtrancl_cases)
lemma subclseq_acyclic:
"\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> \<Longrightarrow> C=D"