equal
deleted
inserted
replaced
790 qed |
790 qed |
791 |
791 |
792 lemma Base_fields_accessible[simp]: |
792 lemma Base_fields_accessible[simp]: |
793 "accfield tprg S Base |
793 "accfield tprg S Base |
794 = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))" |
794 = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))" |
795 apply (auto simp add: accfield_def ext_iff Let_def |
795 apply (auto simp add: accfield_def fun_eq_iff Let_def |
796 accessible_in_RefT_simp |
796 accessible_in_RefT_simp |
797 is_public_def |
797 is_public_def |
798 BaseCl_def |
798 BaseCl_def |
799 permits_acc_def |
799 permits_acc_def |
800 declared_in_def |
800 declared_in_def |
835 by (rule member_of_to_member_in [OF arr_member_of_Ext]) |
835 by (rule member_of_to_member_in [OF arr_member_of_Ext]) |
836 |
836 |
837 lemma Ext_fields_accessible[simp]: |
837 lemma Ext_fields_accessible[simp]: |
838 "accfield tprg S Ext |
838 "accfield tprg S Ext |
839 = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))" |
839 = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))" |
840 apply (auto simp add: accfield_def ext_iff Let_def |
840 apply (auto simp add: accfield_def fun_eq_iff Let_def |
841 accessible_in_RefT_simp |
841 accessible_in_RefT_simp |
842 is_public_def |
842 is_public_def |
843 BaseCl_def |
843 BaseCl_def |
844 ExtCl_def |
844 ExtCl_def |
845 permits_acc_def |
845 permits_acc_def |