src/HOL/Bali/WellForm.thy
changeset 14030 cd928c0ac225
parent 14025 d9b155757dc8
child 14174 f3cafd2929d5
     1.1 --- a/src/HOL/Bali/WellForm.thy	Wed May 14 15:22:37 2003 +0200
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Wed May 14 20:29:18 2003 +0200
     1.3 @@ -509,7 +509,8 @@
     1.4  A program declaration is wellformed if:
     1.5  \begin{itemize}
     1.6  \item the class ObjectC of Object is defined
     1.7 -\item every method of has an access modifier distinct from Package. This is
     1.8 +\item every method of Object has an access modifier distinct from Package. 
     1.9 +      This is
    1.10        necessary since every interface automatically inherits from Object.  
    1.11        We must know, that every time a Object method is "overriden" by an 
    1.12        interface method this is also overriden by the class implementing the
    1.13 @@ -2922,7 +2923,7 @@
    1.14    show ?thesis
    1.15    proof (induct)
    1.16      case (Immediate C m)
    1.17 -    have "G \<turnstile> m in C permits_acc_to accC" and "accmodi m = Private" .
    1.18 +    have "G \<turnstile> m in C permits_acc_from accC" and "accmodi m = Private" .
    1.19      then show ?case
    1.20        by (simp add: permits_acc_def)
    1.21    next
    1.22 @@ -2948,7 +2949,7 @@
    1.23    proof (induct rule: dyn_accessible_fromR.induct)
    1.24      case (Immediate C m)
    1.25      assume "G\<turnstile>m member_in C"
    1.26 -           "G \<turnstile> m in C permits_acc_to accC"
    1.27 +           "G \<turnstile> m in C permits_acc_from accC"
    1.28             "accmodi m = Package"      
    1.29      then show "?P m"
    1.30        by (auto simp add: permits_acc_def)
    1.31 @@ -2987,7 +2988,7 @@
    1.32    show ?thesis
    1.33    proof (induct)
    1.34      case (Immediate C f)
    1.35 -    have "G \<turnstile> f in C permits_acc_to accC" and "accmodi f = Package" .
    1.36 +    have "G \<turnstile> f in C permits_acc_from accC" and "accmodi f = Package" .
    1.37      then show ?case
    1.38        by (simp add: permits_acc_def)
    1.39    next
    1.40 @@ -3011,7 +3012,7 @@
    1.41    show ?thesis
    1.42    proof (induct)
    1.43      case (Immediate C f)
    1.44 -    have "G \<turnstile> f in C permits_acc_to accC" .
    1.45 +    have "G \<turnstile> f in C permits_acc_from accC" .
    1.46      moreover 
    1.47      assume "accmodi f = Protected" and  "is_field f" and "\<not> is_static f" and
    1.48             "pid (declclass f) \<noteq> pid accC"
    1.49 @@ -3039,7 +3040,7 @@
    1.50      assume "accmodi f = Protected" and  "is_field f" and "is_static f" and
    1.51             "pid (declclass f) \<noteq> pid accC"
    1.52      moreover 
    1.53 -    have "G \<turnstile> f in C permits_acc_to accC" .
    1.54 +    have "G \<turnstile> f in C permits_acc_from accC" .
    1.55      ultimately
    1.56      have "G\<turnstile> accC \<preceq>\<^sub>C declclass f"
    1.57        by (auto simp add: permits_acc_def)