--- a/src/HOL/Bali/Decl.thy Wed Mar 28 11:46:14 2012 +0200
+++ b/src/HOL/Bali/Decl.thy Wed Mar 28 12:08:08 2012 +0200
@@ -129,11 +129,12 @@
acc_modi_Package_le acc_modi_le_Package
acc_modi_Protected_le acc_modi_le_Protected
-lemma acc_modi_Package_le_cases
- [consumes 1,case_names Package Protected Public]:
- "Package \<le> m \<Longrightarrow> ( m = Package \<Longrightarrow> P m) \<Longrightarrow> (m=Protected \<Longrightarrow> P m) \<Longrightarrow>
- (m=Public \<Longrightarrow> P m) \<Longrightarrow> P m"
-by (auto dest: acc_modi_Package_le)
+lemma acc_modi_Package_le_cases:
+ assumes "Package \<le> m"
+ obtains (Package) "m = Package"
+ | (Protected) "m = Protected"
+ | (Public) "m = Public"
+using assms by (auto dest: acc_modi_Package_le)
subsubsection {* Static Modifier *}