src/HOL/Bali/TypeSafe.thy
changeset 14700 2f885b7e5ba7
parent 14030 cd928c0ac225
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Sat May 01 22:28:51 2004 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon May 03 23:22:17 2004 +0200
     1.3 @@ -776,12 +776,8 @@
     1.4  apply (force intro: var_tys_Some_eq [THEN iffD2])
     1.5  done
     1.6  
     1.7 -lemma obj_split: "\<And> obj. \<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>"
     1.8 -proof record_split
     1.9 -  fix tag values more
    1.10 -  show "\<exists>t vs. \<lparr>tag = tag, values = values, \<dots> = more\<rparr> = \<lparr>tag = t, values = vs\<rparr>"
    1.11 -    by auto
    1.12 -qed
    1.13 +lemma obj_split: "\<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>"
    1.14 +  by (cases obj) auto
    1.15   
    1.16  lemma AVar_lemma2: "error_free state 
    1.17         \<Longrightarrow> error_free
    1.18 @@ -3602,7 +3598,7 @@
    1.19  	show "G\<turnstile>statC\<preceq>\<^sub>C statDeclC"
    1.20  	  by (auto dest!: accfield_fields dest: fields_declC)
    1.21  	from accfield
    1.22 -	show fld: "table_of (fields G statC) (fn, statDeclC) = Some f"
    1.23 +	show fld: "table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f"
    1.24  	  by (auto dest!: accfield_fields)
    1.25  	from wf show "wf_prog G" .
    1.26  	from conf_a s2 show "x2 = None \<longrightarrow> G,store2\<turnstile>a\<Colon>\<preceq>Class statC"