src/HOL/Bali/TypeRel.thy
changeset 47176 568fdc70e565
parent 46212 d86ef6b96097
child 58887 38db8ddc0f57
--- 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"