equal
deleted
inserted
replaced
127 lemmas acc_modi_le_Dests = acc_modi_top acc_modi_le_Public |
127 lemmas acc_modi_le_Dests = acc_modi_top acc_modi_le_Public |
128 acc_modi_Private_le acc_modi_bottom |
128 acc_modi_Private_le acc_modi_bottom |
129 acc_modi_Package_le acc_modi_le_Package |
129 acc_modi_Package_le acc_modi_le_Package |
130 acc_modi_Protected_le acc_modi_le_Protected |
130 acc_modi_Protected_le acc_modi_le_Protected |
131 |
131 |
132 lemma acc_modi_Package_le_cases |
132 lemma acc_modi_Package_le_cases: |
133 [consumes 1,case_names Package Protected Public]: |
133 assumes "Package \<le> m" |
134 "Package \<le> m \<Longrightarrow> ( m = Package \<Longrightarrow> P m) \<Longrightarrow> (m=Protected \<Longrightarrow> P m) \<Longrightarrow> |
134 obtains (Package) "m = Package" |
135 (m=Public \<Longrightarrow> P m) \<Longrightarrow> P m" |
135 | (Protected) "m = Protected" |
136 by (auto dest: acc_modi_Package_le) |
136 | (Public) "m = Public" |
|
137 using assms by (auto dest: acc_modi_Package_le) |
137 |
138 |
138 |
139 |
139 subsubsection {* Static Modifier *} |
140 subsubsection {* Static Modifier *} |
140 type_synonym stat_modi = bool (* modifier: static *) |
141 type_synonym stat_modi = bool (* modifier: static *) |
141 |
142 |