--- a/src/HOL/Bali/Example.thy Wed May 14 15:22:37 2003 +0200
+++ b/src/HOL/Bali/Example.thy Wed May 14 20:29:18 2003 +0200
@@ -697,7 +697,7 @@
by (rule member_of_to_member_in [OF Ext_foo_member_of_Ext])
lemma Base_foo_permits_acc:
- "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_to S"
+ "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_from S"
by ( simp add: permits_acc_def Base_foo_def)
lemma Base_foo_accessible [simp]:
@@ -720,7 +720,7 @@
done
lemma Ext_foo_permits_acc:
- "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_to S"
+ "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_from S"
by ( simp add: permits_acc_def Ext_foo_def)
lemma Ext_foo_accessible [simp]: