adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

x64: refine: update group lemma

This commit is contained in:
Joel Beeren 2017-04-03 17:48:15 +10:00
parent dd8f8bd33e
commit 53e0f5e476
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/refine/X64/KHeap_R.thy
View File

@ -95,6 +95,8 @@ lemma typ_at_to_obj_at':
lemmas typ_at_to_obj_at_arches
= typ_at_to_obj_at'[where 'a=pte, simplified]
typ_at_to_obj_at' [where 'a=pde, simplified]
typ_at_to_obj_at' [where 'a=pdpte, simplified]
typ_at_to_obj_at' [where 'a=pml4e, simplified]
typ_at_to_obj_at'[where 'a=asidpool, simplified]
typ_at_to_obj_at'[where 'a=user_data, simplified]
typ_at_to_obj_at'[where 'a=user_data_device, simplified]