src/HOL/Bali/WellForm.thy
changeset 14025 d9b155757dc8
parent 13688 a0b16d42d489
child 14030 cd928c0ac225
     1.1 --- a/src/HOL/Bali/WellForm.thy	Tue May 13 08:59:21 2003 +0200
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Wed May 14 10:22:09 2003 +0200
     1.3 @@ -1514,7 +1514,7 @@
     1.4          methd G (super c) sig = Some old\<rbrakk> 
     1.5      \<Longrightarrow> methd G C sig = Some (C,new)"
     1.6  by (auto simp add: methd_rec
     1.7 -            intro: filter_tab_SomeI override_find_right table_of_map_SomeI)
     1.8 +            intro: filter_tab_SomeI map_add_find_right table_of_map_SomeI)
     1.9  
    1.10  lemma wf_prog_staticD:
    1.11    assumes     wf: "wf_prog G" and
    1.12 @@ -1667,8 +1667,7 @@
    1.13  	    by (auto simp add: inherits_def)
    1.14  	  with clsC ws no_new super neq_C_Obj
    1.15  	  have "methd G C sig = Some super_method"
    1.16 -	    by (auto simp add: methd_rec override_def
    1.17 -	                intro: filter_tab_SomeI)
    1.18 +	    by (auto simp add: methd_rec map_add_def intro: filter_tab_SomeI)
    1.19            with None show ?thesis
    1.20  	    by simp
    1.21  	qed