Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Bali/Example.thy
changeset 14030 cd928c0ac225
parent 13688 a0b16d42d489
child 14981 e73f8140af78 
     1.1 --- a/src/HOL/Bali/Example.thy	Wed May 14 15:22:37 2003 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Wed May 14 20:29:18 2003 +0200
     1.3 @@ -697,7 +697,7 @@
     1.4  by (rule member_of_to_member_in [OF Ext_foo_member_of_Ext])
     1.5  
     1.6  lemma Base_foo_permits_acc:
     1.7 - "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_to S"
     1.8 + "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_from S"
     1.9  by ( simp add: permits_acc_def Base_foo_def)
    1.10  
    1.11  lemma Base_foo_accessible [simp]:
    1.12 @@ -720,7 +720,7 @@
    1.13  done
    1.14  
    1.15  lemma Ext_foo_permits_acc:
    1.16 - "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_to S"
    1.17 + "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_from S"
    1.18  by ( simp add: permits_acc_def Ext_foo_def)
    1.19  
    1.20  lemma Ext_foo_accessible [simp]:
isabelle