src/HOL/Bali/Example.thy
changeset 14030 cd928c0ac225
parent 13688 a0b16d42d489
child 14981 e73f8140af78
--- 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]: