| changeset 14700 | 2f885b7e5ba7 |
| parent 14674 | 3506a9af46fc |
| child 14981 | e73f8140af78 |
--- a/src/HOL/Bali/TypeRel.thy Sat May 01 22:28:51 2004 +0200 +++ b/src/HOL/Bali/TypeRel.thy Mon May 03 23:22:17 2004 +0200 @@ -545,7 +545,7 @@ lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object" apply (case_tac T) apply (auto) -apply (subgoal_tac "G\<turnstile>pid_field_type\<preceq>\<^sub>C Object") +apply (subgoal_tac "G\<turnstile>qtname_ext_type\<preceq>\<^sub>C Object") apply (auto intro: subcls_ObjectI) done